diff --git a/_CoqProject b/_CoqProject
index d914ff878dd64dc93325097c297ef93486ca4027..28a244a52fc3f4023e523ab031b6fb6cb2b05dd8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -47,4 +47,5 @@ theories/typing/tests/get_x.v
theories/typing/tests/rebor.v
theories/typing/tests/unbox.v
theories/typing/tests/init_prod.v
+theories/typing/tests/option_as_mut.v
theories/typing/unsafe/cell.v
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index 5b5be8279fabfc7e849d40a5ba712e1df3cb5c90..d8f685623dacec379df2d3ca8d23457f2a99f243 100644
--- a/theories/lang/new_delete.v
+++ b/theories/lang/new_delete.v
@@ -41,10 +41,10 @@ Section specs.
Qed.
End specs.
-(* FIXME : why are these notations not pretty-printed. *)
-Notation "'letalloc:' x := e1 'in' e2" :=
+(* FIXME : why are these notations not pretty-printed? *)
+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" :=
+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 915062ba05a8abba8506803f9d0d5a1923667631..dcd053b6fe9506c548013135d9f256a55109ddfe 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -25,9 +25,9 @@ Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
Notation "'case:' e0 'of' el" := (Case e0%E el%E)
- (at level 102, e0, el at level 200) : expr_scope.
+ (at level 102, e0, el at level 150) : expr_scope.
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.
+ (only parsing, at level 200, e1, e2, e3 at level 150) : expr_scope.
Notation "()" := LitUnit : val_scope.
Notation "! e" := (Read Na1Ord e%E) (at level 9, format "! e") : expr_scope.
Notation "!ˢᶜ e" := (Read ScOrd e%E) (at level 9, format "!ˢᶜ e") : expr_scope.
@@ -65,25 +65,25 @@ Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%V
Notation "'let:' x := e1 'in' e2" :=
((Lam (@cons binder x%RustB nil) e2%E) (@cons expr e1%E nil))
- (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
+ (at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
Notation "e1 ;; e2" := (let: <> := e1 in e2)%E
- (at level 100, e2 at level 200, format "e1 ;; e2") : expr_scope.
+ (at level 100, e2 at level 150, format "e1 ;; e2") : expr_scope.
(* These are not actually values, but we want them to be pretty-printed. *)
Notation "'let:' x := e1 'in' e2" :=
(LamV (@cons binder x%RustB nil) e2%E (@cons expr e1%E nil))
- (at level 102, x at level 1, e1, e2 at level 200) : val_scope.
+ (at level 102, x at level 1, e1, e2 at level 150) : val_scope.
Notation "e1 ;; e2" := (let: <> := e1 in e2)%V
- (at level 100, e2 at level 200, format "e1 ;; e2") : val_scope.
+ (at level 100, e2 at level 150, format "e1 ;; e2") : val_scope.
-Notation "'letcont:' k xl := e1 'in' e2" :=
- ((Lam (@cons binder k%RustB nil) e2%E) [Rec k%RustB xl%RustB e1%E])
- (only parsing, at level 102, k, xl at level 1, e1, e2 at level 200) : expr_scope.
+Notation "e1 'cont:' k xl := e2" :=
+ ((Lam (@cons binder k%RustB nil) e1%E) [Rec k%RustB xl%RustB e2%E])
+ (only parsing, at level 151, k, xl at level 1, e2 at level 150) : expr_scope.
Notation "'call:' f args → k" := (f (@cons expr k args))%E
(only parsing, at level 102, f, args, k at level 1) : expr_scope.
Notation "'letcall:' x := f args 'in' e" :=
- (letcont: "_k" [ x ] := e in call: f args → "_k")%E
- (at level 102, x, f, args at level 1, e at level 200) : expr_scope.
+ (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.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index c282642773ed0f0fe012275a7862edafc9383c8a..fd3731326f68da626495980e91cde3dafd22d7a8 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -19,14 +19,14 @@ Section typing.
rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "* Htl HL HT").
Qed.
- Lemma type_cont argsb L1 T' E L2 C T econt e2 kb :
+ Lemma type_cont argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
- (∀ k args, typed_body E L1 (k â—cont(L1, T') :: C) (T' args)
- (subst_v (kb::argsb) (k:::args) econt)) →
(∀ k, typed_body E L2 (k â—cont(L1, T') :: C) T (subst' kb k e2)) →
- typed_body E L2 C T (letcont: kb argsb := econt in e2).
+ (∀ k (args : vec val (length argsb)),
+ typed_body E L1 (k â—cont(L1, T') :: C) (T' args) (subst_v (kb::argsb) (k:::args) econt)) →
+ typed_body E L2 C T (e2 cont: kb argsb := econt).
Proof.
- iIntros (Hc1 Hc2 Hecont He2) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
+ iIntros (Hc1 Hc2 He2 Hecont) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
{ simpl. rewrite decide_left. done. }
iModIntro. iApply (He2 with "* HEAP LFT Htl HE HL [HC] HT"). clear He2.
iIntros "HE". iLöb as "IH". iIntros (x) "H".
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 0b97434e0d4952aa69802914c234c331d6b4d359..4890d0cf8a681f173d352cfc4af8d2b743e069a6 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -231,9 +231,6 @@ Section typing.
+ by eapply is_closed_weaken, list_subseteq_nil.
+ eapply Is_true_eq_left, forallb_forall, List.Forall_forall, Forall_impl=>//.
intros. eapply Is_true_eq_true, is_closed_weaken=>//. set_solver+.
- - intros k ret. inv_vec ret=>ret. rewrite /subst_v /=.
- rewrite ->(is_closed_subst []), incl_cctx_incl; first done; try set_solver+.
- apply subst'_is_closed; last done. apply is_closed_of_val.
- intros.
(* TODO : make [simpl_subst] work here. *)
change (subst' "_k" k (p (Var "_k" :: ps))) with
@@ -242,6 +239,9 @@ Section typing.
assert (map (subst "_k" k) ps = ps) as ->.
{ clear -Hpsc. induction Hpsc=>//=. rewrite is_closed_nil_subst //. congruence. }
eapply type_call; try done. constructor. done.
+ - move=>/= k ret. inv_vec ret=>ret. rewrite /subst_v /=.
+ rewrite ->(is_closed_subst []), incl_cctx_incl; first done; try set_solver+.
+ apply subst'_is_closed; last done. apply is_closed_of_val.
Qed.
Lemma type_rec {A} E L E' fb (argsb : list binder) e
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index aab3d1c2f56e98c5a1d3845c8af2f1593d0ae739..2093f918a1805b199bdbb1ced97441d0371ab40b 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -444,8 +444,8 @@ Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
[tctx_extract_hasty] to suceed even if the type is an evar, and
merging makes it diverge in this case. *)
Ltac solve_typing :=
- (eauto 100 with lrust_typing typeclass_instances; fail) ||
- (eauto 100 with lrust_typing lrust_typing_merge typeclass_instances; fail).
+ (eauto 100 with lrust_typing typeclass_instances lia; fail) ||
+ (eauto 100 with lrust_typing lrust_typing_merge typeclass_instances lia; fail).
Create HintDb lrust_typing_merge.
Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index c63a3aa6bf48679a3a7764c54cc1c0923a6e7e1e..322a06d32e6417116c0dac0b86dd8645e8b078f4 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -256,7 +256,7 @@ Section typing.
tctx_extract_hasty E L p ty T T' →
ty.(ty_size) = 1%nat →
(∀ (v : val), typed_body E L C ((v ◠own 1 ty)::T') (subst x v e)) →
- typed_body E L C T (letalloc: x := p in e).
+ typed_body E L C T (letalloc: x <- p in e).
Proof.
intros. eapply type_new.
- rewrite /Closed /=. rewrite !andb_True.
@@ -278,7 +278,7 @@ Section typing.
tctx_extract_hasty E L p ty1 T T' →
(∀ (v : val),
typed_body E L C ((v ◠own (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.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index e42e2536f173cfdf302d3d9567d4d70d0a7ed285..d2da2e67386b708d646f2690de53265197c29db7 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -235,6 +235,6 @@ End sum.
(* Σ is commonly used for the current functor. So it cannot be defined
as Î for products. We stick to the following form. *)
Notation "Σ[ ty1 ; .. ; tyn ]" :=
- (sum (cons ty1 (..(cons tyn nil)..))) : lrust_typing.
+ (sum (cons ty1%T (..(cons tyn%T nil)..))) : lrust_type_scope.
Hint Resolve sum_mono' sum_proper' : lrust_typing.
diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index 80f507e37fb9c26ebc5485f284224e188b8f51f8..2140dcaffa0c0b945dc39e45af9af7a5b6552bed 100644
--- a/theories/typing/tests/get_x.v
+++ b/theories/typing/tests/get_x.v
@@ -10,7 +10,7 @@ Section get_x.
Definition get_x : val :=
funrec: <> ["p"] :=
let: "p'" := !"p" in
- letalloc: "r" := "p'" +â‚— #0 in
+ letalloc: "r" <- "p'" +â‚— #0 in
delete [ #1; "p"] ;; "return" ["r"].
Lemma get_x_type :
diff --git a/theories/typing/tests/option_as_mut.v b/theories/typing/tests/option_as_mut.v
new file mode 100644
index 0000000000000000000000000000000000000000..2a735e97fe92fefd1e173d38ed0a0e96816d5cdf
--- /dev/null
+++ b/theories/typing/tests/option_as_mut.v
@@ -0,0 +1,40 @@
+From lrust.lifetime Require Import definitions.
+From lrust.lang Require Import new_delete.
+From lrust.typing Require Import programs product product_split own uniq_bor
+ shr_bor int function lft_contexts uninit cont borrow type_sum.
+Set Default Proof Using "Type".
+
+Section option_as_mut.
+ Context `{typeG Σ}.
+
+ Definition option_as_mut :=
+ (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"] ]
+ cont: "k" ["r"] :=
+ delete [ #1; "o"];; "return" ["r"])%E.
+
+ Lemma option_as_mut_type Ï„ :
+ typed_instruction_ty [] [] [] option_as_mut
+ (fn (λ α, [☀α])%EL (λ α, [# own 1 (&uniq{α}Σ[unit; τ])])
+ (λ α, own 2 (Σ[unit; &uniq{α}τ]))).
+ Proof.
+ apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>o. simpl_subst.
+ eapply (type_cont [_] [] (λ r, [o ◠_; r!!!0 ◠_])%TC) ; try solve_typing.
+ - intros k. simpl_subst.
+ eapply type_deref; try solve_typing; [apply read_own_move|done|]=>o'. simpl_subst.
+ eapply type_case_uniq; try solve_typing. constructor; last constructor; last constructor.
+ + left. eapply type_new; try solve_typing. intros r. simpl_subst.
+ eapply (type_sum_assign_unit [unit; &uniq{α}τ]%T); try solve_typing. by apply write_own.
+ eapply (type_jump [_]); solve_typing.
+ + left. eapply type_new; try solve_typing. intros r. simpl_subst.
+ eapply (type_sum_assign [unit; &uniq{α}τ]%T); try solve_typing. by apply write_own.
+ eapply (type_jump [_]); solve_typing.
+ - move=>/= k r. inv_vec r=>r. simpl_subst.
+ eapply type_delete; try solve_typing.
+ eapply (type_jump [_]); solve_typing.
+ Qed.
+End option_as_mut.
diff --git a/theories/typing/tests/rebor.v b/theories/typing/tests/rebor.v
index 6a8c4a739df35b3ed40c3f3f27f3776e36d56829..39cc4532cc288016f93cf04f7de902612e316679 100644
--- a/theories/typing/tests/rebor.v
+++ b/theories/typing/tests/rebor.v
@@ -10,11 +10,11 @@ Section rebor.
Definition rebor : val :=
funrec: <> ["t1"; "t2"] :=
Newlft;;
- letalloc: "x" := "t1" in
+ letalloc: "x" <- "t1" in
let: "x'" := !"x" in let: "y" := "x'" +â‚— #0 in
"x" <- "t2";;
let: "y'" := !"y" in
- letalloc: "r" := "y'" in
+ letalloc: "r" <- "y'" in
Endlft ;; delete [ #2; "t1"] ;; delete [ #2; "t2"] ;;
delete [ #1; "x"] ;; "return" ["r"].
diff --git a/theories/typing/tests/unbox.v b/theories/typing/tests/unbox.v
index f2af4f94cb5faef1d06e75bce394d123fcb2c0e1..d25078036e826661e272c26287d8b051952392c9 100644
--- a/theories/typing/tests/unbox.v
+++ b/theories/typing/tests/unbox.v
@@ -10,7 +10,7 @@ Section unbox.
Definition unbox : val :=
funrec: <> ["b"] :=
let: "b'" := !"b" in let: "bx" := !"b'" in
- letalloc: "r" := "bx" +â‚— #0 in
+ letalloc: "r" <- "bx" +â‚— #0 in
delete [ #1; "b"] ;; "return" ["r"].
Lemma ubox_type :
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 0e7412d6c3d29bb6accf686d5747f91eaaf4a4d8..93f37f87d7066e8b35da37ca99649996b068c6f0 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -151,12 +151,12 @@ Section case.
apply type_case_shr'; first done. eapply Forall2_impl; first done. auto.
Qed.
- Lemma type_sum_assign {E L} (i : nat) tyl ty1 ty2 ty p1 p2 :
- tyl !! i = Some ty →
+ 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).
Proof.
- iIntros (Hty Hw) "!# * #HEAP #LFT $ HE HL Hp".
+ iIntros (Hw Hty) "!# * #HEAP #LFT $ HE HL Hp".
rewrite tctx_interp_cons tctx_interp_singleton.
iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
@@ -178,7 +178,20 @@ Section case.
iExists i, [_], _. rewrite -Hlen nth_lookup Hty. auto.
Qed.
- Lemma type_sum_assign_unit {E L} (i : nat) tyl ty1 ty2 p :
+ Lemma type_sum_assign {E L} tyl i ty1 ty ty1' C T T' p1 p2 e:
+ Closed [] e →
+ 0 ≤ i →
+ tctx_extract_ctx E L [p1 ◠ty1; p2 ◠ty] T T' →
+ 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).
+ Proof.
+ intros. rewrite -(Z2Nat.id i) //.
+ eapply type_seq; [done|by eapply type_sum_assign_instr|done|done].
+ Qed.
+
+ 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).
@@ -193,7 +206,20 @@ Section case.
iExists i, [], _. rewrite -Hlen nth_lookup Hty. auto.
Qed.
- Lemma type_sum_memcpy {E L} (i : nat) tyl ty1 ty1' ty2 ty2' ty p1 p2 :
+ Lemma type_sum_assign_unit {E L} tyl i ty1 ty1' C T T' p e:
+ Closed [] e →
+ 0 ≤ i →
+ tctx_extract_hasty E L p ty1 T T' →
+ 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).
+ Proof.
+ intros. rewrite -(Z2Nat.id i) //.
+ eapply type_seq; [done|by eapply type_sum_assign_unit_instr|solve_typing|done].
+ Qed.
+
+ Lemma type_sum_memcpy_instr {E L} (i : nat) tyl ty1 ty1' ty2 ty2' ty p1 p2 :
tyl !! i = Some ty →
typed_write E L ty1 (sum tyl) ty1' →
typed_read E L ty2 ty ty2' →
@@ -230,4 +256,19 @@ Section case.
iExists _. iFrame. rewrite /= drop_length. iPureIntro. lia.
- iExists _. iFrame.
Qed.
+
+ Lemma type_sum_assign_memcpy {E L} tyl i ty1 ty2 ty n ty1' ty2' C T T' p1 p2 e:
+ Closed [] e →
+ 0 ≤ i →
+ tctx_extract_ctx E L [p1 ◠ty1; p2 ◠ty2] T T' →
+ typed_write E L ty1 (sum tyl) ty1' →
+ typed_read E L ty2 ty ty2' →
+ 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).
+ Proof.
+ intros ???? Hr ???. subst. rewrite -(Z2Nat.id i) //.
+ by eapply type_seq; [done|eapply type_sum_memcpy_instr, Hr|done|done].
+ Qed.
End case.