Commit 1ea81078 authored by charguer's avatar charguer
Browse files

transfer

parent 98b873ee
......@@ -11,25 +11,32 @@ let create () =
back = [];
size = 0 }
let length s =
s.size
let length q =
q.size
let is_empty s =
s.size = 0
let is_empty q =
q.size = 0
let push x s =
s.back <- x :: s.back;
s.size <- s.size + 1
let push x q =
q.back <- x :: q.back;
q.size <- q.size + 1
let pop s =
if s.front = [] then begin
s.front <- List.rev s.back;
s.back <- [];
let pop q =
if q.front = [] then begin
q.front <- List.rev q.back;
q.back <- [];
end;
match s.front with
match q.front with
| [] -> raise Not_found
| x::f ->
s.front <- f;
s.size <- s.size - 1;
q.front <- f;
q.size <- q.size - 1;
x
(** [transfer q1 q2] adds all of [q1]'s elements at the end
of the queue [q2], then clears [q1] *)
let transfer q1 q2 =
while not (is_empty q1) do
push (pop q1) q2
done
\ No newline at end of file
......@@ -10,3 +10,5 @@ val is_empty : 'a t -> bool
val push : 'a -> 'a t -> unit
val pop : 'a t -> 'a
val transfer : 'a t -> 'a t -> unit
......@@ -21,7 +21,7 @@ Qed.
Definition Queue A (L:list A) (q:t_ A) :=
Hexists (f:list A) (b:list A) (n:int),
q ~> `{ front' := f; back' := b; size' := n }
\* \[ L = f ++ rev b ] \* \[ n = length L ].
\* \[ L = f ++ rev b /\ n = length L ].
(*******************************************************************)
......@@ -30,7 +30,7 @@ Definition Queue A (L:list A) (q:t_ A) :=
Lemma Queue_open : forall q A (L:list A),
q ~> Queue L ==>
Hexists f b n, q ~> `{ front' := f; back' := b; size' := n }
\* \[ L = f ++ rev b ] \* \[ n = length L ].
\* \[ L = f ++ rev b /\ n = length L ].
Proof using.
intros. xunfolds* Queue.
Qed.
......@@ -85,7 +85,7 @@ Lemma length_spec : forall (A:Type) (L:list A) (q:loc),
Proof using.
xcf.
xopen q. (* details: xchange (@Stack_open s). *)
xpull ;=> f b n I1 I2.
xpull ;=> f b n (I1&I2).
xapp. xpull. intros ->.
xclose q. { subst*. } (* details: xchange (@Stack_close s). *)
xsimpl*.
......@@ -93,20 +93,24 @@ Proof using.
Unshelve. solve_type.
Qed.
Hint Extern 1 (RegisterSpec length) => Provide length_spec.
(*******************************************************************)
(** Length *)
(** Is_empty *)
Lemma is_empty_spec : forall A (L:list A) q,
app is_empty [q]
INV (q ~> Queue L)
POST (fun b => \[b = isTrue (L = nil)]).
Proof using.
xcf. xopen q. xpull ;=> f b n I1 I2. xapps. xclose* q. xrets.
xcf. xopen q. xpull ;=> f b n (I1&I2). xapps. xclose* q. xrets.
subst n. rewrite* length_zero_eq_eq_nil.
Unshelve. solve_type.
Qed.
Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
(*******************************************************************)
(** Push *)
......@@ -116,7 +120,7 @@ Lemma push_spec : forall A (L:list A) q x,
PRE (q ~> Queue L)
POST (fun (_:unit) => q ~> Queue (L ++ x::nil)).
Proof using.
xcf. xopen q. xpull. intros f b n I1 I2.
xcf. xopen q. xpull. intros f b n (I1&I2).
xapps. xapp. xapps. xapp.
xclose q. { subst. rew_list. math. }
xsimpl. subst. rew_list*.
......@@ -134,7 +138,7 @@ Lemma pop_spec : forall A (L:list A) q,
PRE (q ~> Queue L)
POST (fun x => Hexists L', \[L = x::L'] \* q ~> Queue L').
Proof using.
introv N. xcf. xopen q. xpull. intros f b n I1 I2.
introv N. xcf. xopen q. xpull. intros f b n (I1&I2).
xapps. xapps. xpolymorphic_eq.
xseq (fun (_:unit) => Hexists f' b',
q ~> `{ front' := f'; back' := b'; size' := n }
......@@ -149,4 +153,31 @@ Proof using.
xsimpl. subst L. rew_list*. } }
Qed.
Hint Extern 1 (RegisterSpec pop) => Provide pop_spec.
(*******************************************************************)
(** Transfer *)
Lemma transfer_spec : forall A (L1 L2:list A) q1 q2,
app transfer [q1 q2]
PRE (q1 ~> Queue L1 \* q2 ~> Queue L2)
POST (fun (_:unit) => q1 ~> Queue (@nil A) \* q2 ~> Queue (L2 ++ L1)).
Proof using.
xcf. xwhile; [|xok]. intros R LR HR. revert L2.
induction_wf IH: (@list_sub A) L1. hide IH.
intros. applys (rm HR).
xlet (fun b => \[b = isTrue (L1 <> nil)] \* q1 ~> Queue L1 \* q2 ~> Queue L2).
{ xapps. xrets. rew_isTrue*. }
intros ->.
xif.
{ destruct L1 as [|x L1']; tryfalse.
xseq. { xapps*. intros L1'' E. inverts E. xapps. }
show IH. xpull.
xapplys* IH. rew_list*. }
{ xret_no_gc. xsimpl. subst. rew_list*. }
Qed.
Hint Extern 1 (RegisterSpec transfer) => Provide transfer_spec.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment