Commit e241b995 authored by charguer's avatar charguer

queue lifted

parent cb27171c
......@@ -46,9 +46,9 @@ Fixpoint MList A `{EA:Enc A} (L:list A) (p:loc) : hprop :=
end.
Notation "'Cell' x q" :=
Notation "'MCell' x q" :=
(Record`{ hd := x; tl := q })
(at level 39, x at level 0, q at level 0).
(at level 19, x at level 0, q at level 0).
......@@ -138,7 +138,7 @@ Global Opaque MList.
Fixpoint MListSeg `{EA:Enc A} (q:loc) (L:list A) (p:loc) : hprop :=
match L with
| nil => \[p = q]
| x::L' => Hexists (p':loc), (p ~> Cell x p') \* (p' ~> MListSeg q L')
| x::L' => Hexists (p':loc), (p ~> MCell x p') \* (p' ~> MListSeg q L')
end.
......@@ -153,7 +153,7 @@ Proof using. intros. xunfold~ MListSeg. Qed.
Lemma MListSeg_cons_eq : forall `{EA:Enc A} p q x (L':list A),
p ~> MListSeg q (x::L') =
Hexists (p':loc), (p ~> Cell x p') \* p' ~> MListSeg q L'.
Hexists (p':loc), (p ~> MCell x p') \* p' ~> MListSeg q L'.
Proof using. intros. xunfold MListSeg at 1. simple~. Qed.
Global Opaque MListSeg.
......@@ -163,11 +163,11 @@ Lemma MListSeg_nil : forall `{EA:Enc A} p,
Proof using. intros. rewrite MListSeg_nil_eq. hsimpl~. Qed.
Lemma MListSeg_cons : forall `{EA:Enc A} p p' q x (L':list A),
p ~> (Cell x p') \* p' ~> MListSeg q L' ==> p ~> MListSeg q (x::L').
p ~> (MCell x p') \* p' ~> MListSeg q L' ==> p ~> MListSeg q (x::L').
Proof using. intros. rewrite MListSeg_cons_eq. hsimpl. Qed.
Lemma MListSeg_one : forall `{EA:Enc A} p q (x:A),
p ~> (Cell x q) ==> p ~> MListSeg q (x::nil).
p ~> (MCell x q) ==> p ~> MListSeg q (x::nil).
Proof using.
intros. hchange (MListSeg_nil q). hchanges (>> MListSeg_cons p).
Qed.
......@@ -191,7 +191,7 @@ Proof using.
Qed.
Lemma MListSeg_last : forall `{EA:Enc A} p1 p2 p3 x (L:list A),
p1 ~> MListSeg p2 L \* p2 ~> (Cell x p3) ==> p1 ~> MListSeg p3 (L&x).
p1 ~> MListSeg p2 L \* p2 ~> (MCell x p3) ==> p1 ~> MListSeg p3 (L&x).
Proof using.
intros. hchange (>> MListSeg_one p2). hchanges (>> (@MListSeg_concat) p1 p2).
Qed.
......@@ -218,7 +218,7 @@ Definition val_new_cell :=
Lemma Rule_new_cell : forall `{EA:Enc A} (x:A) (q:loc),
Triple (val_new_cell `x `q)
PRE \[]
POST (fun p => (p ~> Cell x q)).
POST (fun p => (p ~> MCell x q)).
Proof using. xrule_new_record. Qed.
Hint Extern 1 (Register_Spec val_new_cell) => Provide Rule_new_cell.
......@@ -226,8 +226,65 @@ Hint Extern 1 (Register_Spec val_new_cell) => Provide Rule_new_cell.
Opaque val_new_cell.
(* ---------------------------------------------------------------------- *)
(* ** List copy *)
(* ********************************************************************** *)
(* * Mutable queue *)
Definition MQueue `{EA:Enc A} (L:list A) (p:loc) :=
Hexists (pf:loc), Hexists (pb:loc), Hexists (vx:A), Hexists (vy:loc),
p ~> MCell pf pb \* pf ~> MListSeg pb L \* pb ~> MCell vx vy.
(* Same as in [ExampleQueueNonlifted.v] *)
Definition val_is_empty :=
ValFun 'p :=
Let 'x := val_get_hd 'p in
Let 'y := val_get_tl 'p in
val_eq 'x 'y.
Parameter Rule_is_empty : forall `{EA:Enc A} (L:list A) p,
Triple (val_is_empty p)
(p ~> MQueue L)
(fun r => \[r = isTrue (L = nil)] \* p ~> MQueue L).
(* LATER: similar proof to ExampleQueueNonLifted, todo *)
Hint Extern 1 (Register_Spec val_is_empty) => Provide Rule_is_empty.
Definition val_transfer :=
ValFun 'p1 'p2 :=
Let 'e2 := val_is_empty 'p2 in
If_ val_not 'e2 Then
Let 'b1 := val_get_tl 'p1 in
Let 'f2 := val_get_hd 'p2 in
Let 'x2 := val_get_hd 'f2 in
Let 'n2 := val_get_tl 'f2 in
Let 'b2 := val_get_tl 'p2 in
val_set_tl 'p1 'b2 ;;
val_set_hd 'b1 'x2 ;;
val_set_tl 'b1 'n2 ;;
val_set_tl 'p2 'f2
End.
Lemma Rule_transfer : forall `{EA:Enc A} (L1 L2:list A) p1 p2,
Triple (val_transfer p1 p2)
(p1 ~> MQueue L1 \* p2 ~> MQueue L2)
(fun (_:unit) => p1 ~> MQueue (L1 ++ L2) \* p2 ~> MQueue nil).
Proof using.
xcf. xapps. xapps. xif ;=> C.
{ xunfold MQueue. xpull ;=> pf2 pb2 vx2 vy2 pf1 pb1 vx1 vy1.
destruct L2 as [|x L2']; tryfalse.
rewrite MListSeg_cons_eq. xpull ;=> pf2'.
xapps. xapps. xapps. xapps.
xapps~. xapps~. xapps~. xapps~. xapps~.
hchange (>> (@MListSeg_last) pf1).
hchange (MListSeg_concat pf1 pf2'). rew_list.
hchange (MListSeg_nil pf2). hsimpl~. }
{ subst. rew_list. xvals~. }
Qed.
(* ********************************************************************** *)
(* * List Copy *)
Definition val_mlist_copy :=
ValFix 'f 'p :=
......
(* TODO
(** Useful for queues *)
Lemma MCell_eq : forall `{EA1:Enc A1} `{EA2:Enc A2} (v:A1) (q:A2) (p:loc),
(p ~> MCell v q) = (p `.` hd ~~> v) \* (p `.` tl ~~> q).
Proof using.
intros. do 2 rewrite Record_cons. rewrite Record_nil. hsimpl.
Qed.
Lemma MCell_hstar_MCell_inv : forall `{EA1:Enc A1} `{EA2:Enc A2} (p1 p2:loc) (x1 x2:A1) (y1 y2:A2),
p1 ~> MCell x1 y1 \* p2 ~> MCell x2 y2 ==+> \[p1 <> p2].
Proof using.
Admitted.
(*
intros. rewrite MCell_eq. tests C: (p1 = p2).
{ unfold Hfield. repeat xunfold at 1.
rewrite Record_cons. hchanges (@hstar_hfield_same_loc_disjoint p2 hd). }
{ hsimpl~. }
*)
Lemma MListSeg_then_MCell_inv_neq : forall `{EA:Enc A} `{EA1:Enc A1} `{EA2:Enc A2},
forall (p q:loc) (L:list A) (v1:A1) (v2:A2),
p ~> MListSeg q L \* q ~> MCell v1 v2 ==+> \[L = nil <-> p = q].
Proof using.
Admitted.
(*
intros. destruct L.
{ rewrite MListSeg_nil_eq. hsimpl*. split*. (* TODO: why not proved? *) }
{ rewrite MListSeg_cons_eq. hpull ;=> p'. tests: (p = q).
{ lets: (>> MCell_hstar_MCell_inv q q v1 a v2 p'). }
{ hsimpl. split; auto_false. } }
Qed.
*)
(*
Proof using.
xcf. xunfold MQueue. xpull ;=> pf pb vx vy.
xapps. xapps.
xchanges (>> MListSeg_then_MCell_inv_neq pf pb). ;=> R.
(* xchange (MListSeg_then_MCell_inv_neq pf pb). xpull ;=> R. *)
xapp. hsimpl. isubst. fequals. rew_bool_eq. rewrite R. iff; congruence.
Qed.
*)
*)
\ No newline at end of file
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