Type-checking option_as_mut.

_CoqProject

@@ -47,3 +47,4 @@ 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/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.

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.

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".

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

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.

theories/typing/own.v

@@ -254,7 +254,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.
@@ -276,7 +276,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.

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.

theories/typing/tests/get_x.v

@@ -10,7 +10,7 @@ Section get_x.
   Definition get_x :=
     (funrec: <> ["p"] :=
        let: "p'" := !"p" in
-       letalloc: "r" := "p'" +ₗ #0 in
+       letalloc: "r" <- "p'" +ₗ #0 in
        delete [ #1; "p"] ;; "return" ["r":expr])%E.
 
   Lemma get_x_type :

theories/typing/tests/option_as_mut.v

+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.

theories/typing/tests/rebor.v

@@ -10,11 +10,11 @@ Section rebor.
   Definition rebor :=
     (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":expr])%E.
 

theories/typing/tests/unbox.v

@@ -10,7 +10,7 @@ Section unbox.
   Definition unbox :=
     (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":expr])%E.
 
   Lemma ubox_type :

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.