Rc::drop code

theories/typing/fixpoint.v

@@ -41,8 +41,8 @@ Section fixpoint.
       eapply (limit_preserving_ext (λ _, _ ∧ _)).
       { split; (intros [H1 H2]; split; [apply H1|apply H2]). }
       apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
-      { apply uPred.limit_preserving_PersistentP; solve_proper. }
-      apply limit_preserving_impl, uPred.limit_preserving_entails;
+      + apply uPred.limit_preserving_PersistentP; solve_proper.
+      + apply limit_preserving_impl, uPred.limit_preserving_entails;
         solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
   Qed.
 

theories/typing/lib/option.v

@@ -12,8 +12,8 @@ Section option.
       let: "o'" := !"o" in
       let: "r" := new [ #2 ] in
       case: !"o'" of
-        [ "r" <-{Σ 0} ();; "k" ["r"];
-          "r" <-{Σ 1} "o'" +ₗ #1;; "k" ["r"] ]
+        [ "r" <-{Σ 0} ();; "k" [];
+          "r" <-{Σ 1} "o'" +ₗ #1;; "k" [] ]
       cont: "k" ["r"] :=
         delete [ #1; "o"];; return: ["r"].
 

theories/typing/lib/rc.v

@@ -5,7 +5,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import typing.
+From lrust.typing Require Import typing option.
 Set Default Proof Using "Type".
 
 Definition rc_stR :=
@@ -276,4 +276,25 @@ Section code.
     iApply (type_jump [ #_ ]); solve_typing.
   Qed.
 
+  Definition rc_drop ty : val :=
+    funrec: <> ["rc"] :=
+      let: "x" := new [ #(option ty).(ty_size) ] in
+      let: "rc'" := !"rc" in
+      let: "count" := (!"rc'" +ₗ #0) in
+      "rc'" +ₗ #0 <- "count" - #1;;
+      if: "count" = #1 then
+        (* Return content, delete Rc heap allocation. *)
+        "x" <-{ty.(ty_size),Σ 1} !("rc'" +ₗ #1);;
+        delete [ #(S ty.(ty_size)); "rc'" ];;
+        "k" ["x"]
+      else
+        "x" <-{Σ 0} ();;
+        "k" ["x"]
+      cont: "k" ["x"] :=
+        delete [ #1; "rc"];; return: ["x"].
+
+  Lemma rc_drop_type ty :
+    typed_val (rc_drop ty) (fn([]; rc ty) → option ty).
+  Proof. Abort.
+
 End code.