Commit 762975c3 authored by charguer's avatar charguer

minor fixes

parent 8aa15e2a
......@@ -105,7 +105,7 @@ Qed.
Definition val_repeat : val :=
Vars N, F, I in
ValFun N F :=
For I = 1 To N Do
For I := 1 To N Do
F '()
Done.
......
......@@ -48,7 +48,7 @@ Fixpoint MList A `{EA:Enc A} (L:list A) (p:loc) : hprop :=
Notation "'Cell' x q" :=
(Record`{ hd := x; tl := q })
(at level 69, x at level 0, q at level 0).
(at level 39, x at level 0, q at level 0).
......@@ -132,6 +132,73 @@ Global Opaque MList.
(* ---------------------------------------------------------------------- *)
(** Representation *)
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')
end.
(* ---------------------------------------------------------------------- *)
(** Properties *)
Section SegProperties.
Lemma MListSeg_nil_eq : forall `{EA:Enc A} p q,
p ~> (MListSeg q (@nil A)) = \[p = q].
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'.
Proof using. intros. xunfold MListSeg at 1. simple~. Qed.
Global Opaque MListSeg.
Lemma MListSeg_nil : forall `{EA:Enc A} p,
\[] ==> p ~> MListSeg p (@nil A).
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').
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).
Proof using.
intros. hchange (MListSeg_nil q). hchanges (>> MListSeg_cons p).
Qed.
Lemma MListSeg_to_MList : forall `{EA:Enc A} p (L:list A),
p ~> MListSeg null L ==> p ~> MList L.
Proof using.
intros. gen p. induction L; intros.
{ rewrite MListSeg_nil_eq. rewrite MList_nil_eq. auto. }
{ rewrite MListSeg_cons_eq. rewrite MList_cons_eq.
hpull ;=> p'. hchange IHL. hsimpl~. }
Qed.
Lemma MListSeg_concat : forall `{EA:Enc A} p1 p2 p3 (L1 L2:list A),
p1 ~> MListSeg p2 L1 \* p2 ~> MListSeg p3 L2 ==> p1 ~> MListSeg p3 (L1++L2).
Proof using.
intros. gen p1. induction L1 as [|x L1']; intros.
{ rewrite MListSeg_nil_eq. hpull ;=> E. subst. rew_list~. }
{ rew_list. hchange (MListSeg_cons_eq p1). hpull ;=> p1'.
hchange (IHL1' p1'). hchanges (>> MListSeg_cons p1). }
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).
Proof using.
intros. hchange (>> MListSeg_one p2). hchanges (>> (@MListSeg_concat) p1 p2).
Qed.
End SegProperties.
(* ---------------------------------------------------------------------- *)
(* ** Node allocation *)
......@@ -248,6 +315,36 @@ Proof using.
Qed.
(* ********************************************************************** *)
(* * Out-of-place append of two aliased mutable lists *)
Lemma Rule_mlist_append_aliased : forall (L:list int) (p1:loc),
Triple (val_mlist_append `p1 `p1)
PRE (p1 ~> MList L)
POST (fun (p:loc) => p ~> MList (L++L) \* p1 ~> MList L).
Proof using.
cuts K: (forall (L L1 L2:list int) (p1 p3:loc),
L = L1++L2 ->
Triple (val_mlist_append `p3 `p1)
PRE (p1 ~> MListSeg p3 L1 \* p3 ~> MList L2)
POST (fun (p:loc) => p ~> MList (L2++L) \* p1 ~> MList L)).
{ intros. xchange (MListSeg_nil p1). xapplys (K L nil L). rew_list~. }
intros. gen p3 L1. induction_wf: list_sub_wf L2; intros. xcf.
xapps~. xif ;=> C.
{ subst. xchanges MList_null_inv ;=> EL. subst. rew_list.
rewrite MList_nil_eq. xpull ;=> _.
xchange (>> (@MListSeg_to_MList int) p1).
xapp. intros p. rew_list. hsimpl. }
{ xchanges~ (MList_not_null_inv_cons p3) ;=> x p3' L2' EL2.
xapps. xapps.
xchange (>> (@MListSeg_last int) p1).
xapp~ (>> IH L2' (L1&x)) as p'. xapps.
intros p. hchange~ (>> (@MList_cons) p Enc_int).
subst. rew_list. hsimpl. }
Qed.
(* ********************************************************************** *)
(* * Iter *)
......
......@@ -216,7 +216,8 @@ Proof using. intros. fequals. Qed.
(* ** Disjointness *)
Lemma fmap_disjoint_sym : forall h1 h2,
\# h1 h2 -> \# h2 h1.
\# h1 h2 ->
\# h2 h1.
Proof using. intros [f1 F1] [f2 F2]. apply map_disjoint_sym. Qed.
Lemma fmap_disjoint_comm : forall h1 h2,
......
......@@ -168,7 +168,7 @@ Qed.
*)
(** [xfor] applies to a goal of the form [(For i = a To b Do F) H Q].
(** [xfor] applies to a goal of the form [(For i := a To b Do F) H Q].
It introduces an abstract local predicate [S] such that [S i]
denotes the behavior of the loop starting from index [i].
The initial goal is [S a H Q]. An assumption is provided to unfold
......@@ -221,7 +221,7 @@ Qed.
/\ (I (b+1) \* H' ==> Q tt \* \GC)) ->
((a > b) ->
(H ==> Q tt \* \GC)) ->
(For i = a To b Do F i Done_) H Q.
(For i := a To b Do F i Done_) H Q.
Proof using.
introv M1 M2. apply local_erase. intros S LS HS.
tests: (a <= b).
......@@ -240,7 +240,7 @@ Qed.
(a <= b+1) ->
(H ==> I a \* H') ->
(forall i, a <= i <= b -> F i (I i) (# I(i+1))) ->
(For i = a To b Do F i Done_) H (# I (b+1) \* H').
(For i := a To b Do F i Done_) H (# I (b+1) \* H').
Proof using.
introv ML MH MI. applys xfor_inv_case_lemma I; intros C.
{ exists H'. splits~. xsimpl. }
......@@ -252,7 +252,7 @@ Qed.
(a <= n) ->
(H ==> I a \* H') ->
(forall i, a <= i < n -> F i (I i) (# I(i+1))) ->
(For i = a To (n - 1) Do F i Done_) H (# I n \* H').
(For i := a To (n - 1) Do F i Done_) H (# I n \* H').
Proof using.
introv ML MH MI. applys xfor_inv_case_lemma I; intros C.
{ exists H'. splits~.
......@@ -264,7 +264,7 @@ Qed.
Lemma xfor_inv_void_lemma :
forall (a:int) (b:int) (F:int->~~unit) H,
(a > b) ->
(For i = a To b Do F i Done_) H (# H).
(For i := a To b Do F i Done_) H (# H).
Proof using.
introv ML.
applys xfor_inv_case_lemma (fun (i:int) => \[]); intros C.
......
......@@ -352,10 +352,10 @@ Notation "'While' t1 'Do' t2 'Done'" :=
format "'[v' 'While' t1 'Do' '/' '[' t2 ']' '/' 'Done' ']'")
: trm_scope.
Notation "'For' x '=' t1 'To' t2 'Do' t3 'Done'" :=
Notation "'For' x ':=' t1 'To' t2 'Do' t3 'Done'" :=
(trm_for x t1 t2 t3)
(at level 69, x ident, (* t1 at level 0, t2 at level 0, *)
format "'[v' 'For' x '=' t1 'To' t2 'Do' '/' '[' t3 ']' '/' 'Done' ']'")
format "'[v' 'For' x ':=' t1 'To' t2 'Do' '/' '[' t3 ']' '/' 'Done' ']'")
: trm_scope.
......
......@@ -308,7 +308,7 @@ Definition val_array_make : val :=
ValFun N V :=
Let P := val_alloc N in
Let B := val_sub N 1 in
For I = 0 To B Do (* todo: allow inlining of B *)
For I := 0 To B Do (* todo: allow inlining of B *)
Array' P`[I] `<- V
Done;;
P.
......
......@@ -180,7 +180,7 @@ Notation "\[ P ]" := (hpure P)
(** The "Top" predicate, written [\Top], which holds of any heap,
implemented as [Hexists H, H]. *)
Definition htop :=
Definition htop : hprop :=
hexists (fun (H:hprop) => H).
Notation "\Top" := (htop) : heap_scope.
......
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