Commit ee19f69b authored by charguer's avatar charguer

swap

parent 29925162
......@@ -367,6 +367,11 @@ Notation "'RegisterSpecApp' t" := (RegisterSpec (app t _ _))
Tactic Notation "xspec" constr(G) :=
ltac_database_get database_spec G.
(** [xspec] calls [xspec G] on the current goal. *)
Tactic Notation "xspec" :=
match goal with |- ?G => xspec G end.
(* ---------------------------------------------------------------------- *)
(** ** Registering specification of primitive functions *)
......@@ -426,7 +431,7 @@ Tactic Notation "xapp" constr(E) :=
applys local_erase; xapplys E.
Tactic Notation "xapp" :=
applys local_erase;
try applys local_erase;
let G := match goal with |- ?G => constr:(G) end in
xspec G;
let H := fresh "TEMP" in intros H;
......@@ -446,55 +451,59 @@ Tactic Notation "xvals" "*" :=
(** [xapp] and [xapps] and [xapp as] *)
Ltac xapp_cont tt :=
Ltac xapp_let_cont tt :=
let X := fresh "X" in intros X;
instantiate; try xpull; gen X.
Ltac xapp_as_cont tt :=
Ltac xapp_as_let_cont tt :=
instantiate; try xpull.
Ltac xapps_cont tt :=
Ltac xapps_let_cont tt :=
let X := fresh "X" in intros X;
instantiate; try xpull;
first [ intro_subst | gen X ].
Ltac xapp_template xlet_tactic xapp_tactic cont :=
Ltac xapp_template xlet_tactic xapp_tactic xlet_cont :=
match goal with
| |- local (cf_let _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | cont tt ]
| |- local (cf_if _ _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | cont tt ]
| |- local (cf_seq _ _) _ _ => xseq; [ xapp_tactic tt | cont tt ]
| |- local (cf_let _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | xlet_cont tt ]
| |- local (cf_if _ _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | xlet_cont tt ]
| |- local (cf_seq _ _) _ _ => xseq; [ xapp_tactic tt | ]
| _ => xapp_tactic tt
end.
Ltac xapp_basic_prepare tt :=
try match goal with |- triple ?t ?H ?Q => change (app t H Q) end;
try match goal with |- local _ _ _ => apply local_erase end.
Ltac xapp_arg_basic E tt :=
applys local_erase; xapplys E.
xapp_basic_prepare tt;
xapplys E.
Ltac xapp_basic tt :=
applys local_erase;
let G := match goal with |- ?G => constr:(G) end in
xspec G;
let H := fresh "TEMP" in intros H;
xapp_basic_prepare tt;
xspec;
let H := fresh "TEMP" in
intros H;
xapplys H;
clear H.
Ltac xapp_core tt :=
xapp_template ltac:(fun tt => xlet) ltac:(xapp_basic) ltac:(xapp_cont).
xapp_template ltac:(fun tt => xlet) ltac:(xapp_basic) ltac:(xapp_let_cont).
Ltac xapp_arg_core E :=
xapp_template ltac:(fun tt => xlet) ltac:(xapp_arg_basic E) ltac:(xapp_cont).
xapp_template ltac:(fun tt => xlet) ltac:(xapp_arg_basic E) ltac:(xapp_let_cont).
Ltac xapp_as_core X :=
xapp_template ltac:(fun tt => xlet X) ltac:(xapp_basic) ltac:(xapp_as_cont).
xapp_template ltac:(fun tt => xlet X) ltac:(xapp_basic) ltac:(xapp_as_let_cont).
Ltac xapp_arg_as_core E X :=
xapp_template ltac:(fun tt => xlet X) ltac:(xapp_arg_basic E) ltac:(xapp_as_cont).
xapp_template ltac:(fun tt => xlet X) ltac:(xapp_arg_basic E) ltac:(xapp_as_let_cont).
Ltac xapps_core tt :=
xapp_template ltac:(fun tt => xlet) ltac:(xapp_basic) ltac:(xapps_cont).
xapp_template ltac:(fun tt => xlet) ltac:(xapp_basic) ltac:(xapps_let_cont).
Ltac xapps_arg_core E :=
xapp_template ltac:(fun tt => xlet) ltac:(xapp_arg_basic E) ltac:(xapps_cont).
xapp_template ltac:(fun tt => xlet) ltac:(xapp_arg_basic E) ltac:(xapps_let_cont).
Tactic Notation "xapp" :=
xapp_core tt.
......
This diff is collapsed.
......@@ -142,8 +142,7 @@ Lemma rule_incr_4 : forall p n,
(p ~~> n)
(fun r => \[r = val_unit] \* (p ~~> (n+1))).
Proof using.
xcf.
xlet x. xapp. xpull. intro_subst.
xcf. xlet x. xapp. xpull. intro_subst.
xlet y. xapp. xpull. intro_subst.
xapp. auto.
Qed.
......@@ -158,10 +157,40 @@ Proof using.
xcf. xapps. xapps. xapp~.
Qed.
Hint Extern 1 (RegisterSpec (app (trm_app_val val_incr ?x) ?H ?Q)) =>
Hint Extern 1 (RegisterSpecApp (trm_app_val val_incr ?x)) =>
Provide rule_incr.
(* ---------------------------------------------------------------------- *)
(** Calling incr from a larger context *)
Lemma rule_incr_with_other_1 : forall p n q m,
triple (val_incr p)
(p ~~> n \* q ~~> m)
(fun r => \[r = val_unit] \* (p ~~> (n+1)) \* q ~~> m).
Proof using.
intros. applys rule_frame' (q ~~> m).
{ hsimpl. }
{ rew_heap. apply rule_incr. }
{ intros r. hsimpl. auto. }
Qed.
Lemma rule_incr_with_other_2 : forall p n q m,
triple (val_incr p)
(p ~~> n \* q ~~> m)
(fun r => \[r = val_unit] \* (p ~~> (n+1)) \* q ~~> m).
Proof using.
intros. xapply rule_incr.
{ hsimpl. }
{ intros r. hsimpl. auto. }
Qed.
Lemma rule_incr_with_other : forall p n q m,
triple (val_incr p)
(p ~~> n \* q ~~> m)
(fun r => \[r = val_unit] \* (p ~~> (n+1)) \* q ~~> m).
Proof using. intros. xapp~. Qed.
(* ---------------------------------------------------------------------- *)
(** Disequality test *)
......@@ -200,11 +229,45 @@ Proof using.
xcf. xapps. xif ;=> C; case_if; xvals~.
Qed.
Hint Extern 1 (RegisterSpec (app (trm_app2_val val_neq ?x ?y) ?H ?Q)) =>
Hint Extern 1 (RegisterSpecApp (trm_app2_val val_neq ?x ?y)) =>
Provide rule_neq.
(* ---------------------------------------------------------------------- *)
(** Swap function *)
Definition val_swap :=
ValFun P Q :=
Let X := prim_get P in
Let Y := prim_get Q in
prim_set P Y ;;
prim_set Q X.
Ltac hcancel_hook H ::=
match H with
| hsingle _ _ => hcancel_try_same tt
| hfield _ _ _ => hcancel_try_same tt
end.
Lemma rule_swap_neq : forall p q v w,
triple (val_swap p q)
(p ~~> v \* q ~~> w)
(fun r => \[r = val_unit] \* p ~~> w \* q ~~> v).
Proof using.
xcf. xapps. xapps. xapp~. xapp~.
Qed.
Lemma rule_swap_eq : forall p v,
triple (val_swap p p)
(p ~~> v)
(fun r => \[r = val_unit] \* p ~~> v).
Proof using.
xcf. xapps. xapps. xapp~. xapp~.
Qed.
(* ********************************************************************** *)
......
......@@ -18,6 +18,15 @@ Ltac auto_star ::= jauto.
Local Open Scope fmap_scope.
(* ---------------------------------------------------------------------- *)
(* todo: reuse Coq's notation for lsits *)
Notation "'[' x1 ']'" := (x1::nil) : list_scope.
Notation "'[' x1 ; x2 ']'" := (x1::x2::nil) : list_scope.
Notation "'[' x1 ; x2 ; x3 ']'" := (x1::x2::x3::nil) : list_scope.
Notation "'[' x1 ; x2 ; x3 ; x4 ']'" := (x1::x2::x3::x4::nil) : list_scope.
Open Scope list_scope.
Lemma rule_frame' : forall H2 H1 Q1 t H Q,
......@@ -327,3 +336,119 @@ s := p;
done;
!s
*)
(** Record contents *)
(* TODO: use MLCFlifted *)
Notation "`'{ f1 := x1 }" :=
((f1, Dyn x1)::nil)
(at level 0, f1 at level 0)
: trm_scope.
Notation "`'{ f1 := x1 ; f2 := x2 }" :=
((f1, Dyn x1)::(f2, Dyn x2)::nil)
(at level 0, f1 at level 0, f2 at level 0)
: trm_scope.
Notation "`'{ f1 := x1 ; f2 := x2 ; f3 := x3 }" :=
((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0)
: trm_scope.
Notation "`'{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }" :=
((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::(f4, Dyn x4)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
: trm_scope.
Open Scope trm_scope.
(*
Definition hd : field := 0.
Definition tl : field := 1.
*)
Fixpoint MList A `{EA:Enc A} (L:list A) (p:loc) : hprop :=
match L with
| nil => \[p = null]
| x::L' => Hexists (p':loc), (p ~> Record`'{ hd := x; tl := p' }) \* (p' ~> MList L')
end.
Section Properties.
Context (A:Type) `{EA:Enc A}.
Implicit Types L : list A.
Implicit Types p : loc.
(** Conversion lemmas for empty lists *)
Lemma MList_nil : forall p,
p ~> MList nil = \[p = null].
Proof using. intros. xunfold~ MList. Qed.
Lemma MList_unnil :
\[] ==> null ~> MList nil.
Proof using. intros. rewrite MList_nil. hsimpl~. Qed.
Lemma MList_null : forall L,
(null ~> MList L) = \[L = nil].
Proof using.
intros. destruct L.
{ xunfold MList. applys himpl_antisym; hsimpl~. }
{ xunfold MList. applys himpl_antisym.
{ hpull ;=> p'. hchange (hRecord_not_null null); auto_false.
hpull; auto_false. }
{ hpull. } }
Qed.
Lemma MList_null_keep : forall L,
null ~> MList L ==>
null ~> MList L \* \[L = nil].
Proof using.
intros. destruct L.
{ hsimpl~. }
{ rewrite MList_null. hsimpl. }
Qed.
(** Conversion lemmas for non-empty lists *)
Lemma MList_cons : forall p x L',
p ~> MList (x::L') =
Hexists p', (p ~> Record`'{ hd := x; tl := p' }) \* p' ~> MList L'.
Proof using. intros. xunfold MList at 1. simple~. Qed.
Lemma MList_uncons : forall p p' x L',
(p ~> Record`'{ hd := x; tl := p' }) \* p' ~> MList L' ==>
p ~> MList (x::L').
Proof using. intros. rewrite MList_cons. hsimpl. Qed.
Lemma MList_not_null_keep : forall p L,
p <> null ->
p ~> MList L ==> p ~> MList L \* \[L <> nil].
Proof using.
intros. destruct L.
{ hchanges -> (MList_nil p). }
{ hsimpl. auto_false. }
Qed.
Lemma MList_not_null : forall p L,
p <> null ->
p ~> MList L ==> Hexists x p' L',
\[L = x::L']
\* (p ~> Record`'{ hd := x; tl := p' })
\* p' ~> MList L'.
Proof using.
intros. hchange~ (@MList_not_null_keep p). hpull. intros.
destruct L; tryfalse.
hchange (MList_cons p). hsimpl~.
Qed.
End Properties.
Implicit Arguments MList_null_keep [A [EA]].
Implicit Arguments MList_cons [A [EA]].
Implicit Arguments MList_uncons [A [EA]].
Implicit Arguments MList_not_null [A [EA]].
Implicit Arguments MList_not_null_keep [A [EA]].
Global Opaque MList.
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