From a99ee48819c5863d035921d13d866c8b61b9af83 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 10 Mar 2017 10:08:26 +0100
Subject: [PATCH] Rc::drop code
---
theories/typing/fixpoint.v | 4 ++--
theories/typing/lib/option.v | 4 ++--
theories/typing/lib/rc.v | 23 ++++++++++++++++++++++-
3 files changed, 26 insertions(+), 5 deletions(-)
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index e2f2e057..59bb90bf 100644
--- a/theories/typing/fixpoint.v
+++ b/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.
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 720310ac..9ebe8045 100644
--- a/theories/typing/lib/option.v
+++ b/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"].
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index c2405089..c83a2b99 100644
--- a/theories/typing/lib/rc.v
+++ b/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.
--
GitLab