Commit 8fd9621d authored by charguer's avatar charguer

array_lifted

parent 956ab3f7
......@@ -60,9 +60,6 @@ Qed.
(* ---------------------------------------------------------------------- *)
(** Basic two references *)
Global Opaque Z.mul. (* TODO URGENT *)
Global Opaque Z.add.
(** [val_example_let] defined in [ExampleBasicNonLifted.v] *)
Lemma Rule_val_example_let : forall n,
......
......@@ -252,32 +252,6 @@ Qed.
(* ---------------------------------------------------------------------- *)
(** Basic let-binding example *)
Notation "t1 '+ t2" :=
(val_add t1 t2)
(at level 69) : trm_scope.
Notation "t1 '- t2" :=
(val_sub t1 t2)
(at level 69) : trm_scope.
Notation "'ref t" :=
(val_ref t)
(at level 67) : trm_scope.
Notation "'! t" :=
(val_get t)
(at level 67) : trm_scope.
Notation "t1 ':= t2" :=
(val_set t1 t2)
(at level 67) : trm_scope.
Opaque Z.mul.
Opaque Z.add.
(* URGENT: move *)
Definition val_example_let :=
ValFun 'n :=
Let 'a := 'n '+ 1 in
......
......@@ -476,6 +476,29 @@ Notation "'For' x ':=' t1 'To' t2 'Do' t3 'Done'" :=
format "'[v' 'For' x ':=' t1 'To' t2 'Do' '/' '[' t3 ']' '/' 'Done' ']'")
: trm_scope.
Notation "'ref t" :=
(val_ref t)
(at level 67) : trm_scope.
Notation "'! t" :=
(val_get t)
(at level 67) : trm_scope.
Notation "t1 ':= t2" :=
(val_set t1 t2)
(at level 67) : trm_scope.
Notation "t1 '+ t2" :=
(val_add t1 t2)
(at level 69) : trm_scope.
Notation "t1 '- t2" :=
(val_sub t1 t2)
(at level 69) : trm_scope.
Notation "t1 '= t2" :=
(val_eq t1 t2)
(at level 69) : trm_scope.
(* ********************************************************************** *)
......
......@@ -38,7 +38,7 @@ Implicit Types n : int.
Definition val_incr :=
ValFun 'p :=
Let 'n := val_get 'p in
Let 'm := val_add 'n 1 in
Let 'm := 'n '+ 1 in
val_set 'p 'm.
(** Same proof using characteristic formulae with advanced tactics *)
......@@ -58,7 +58,7 @@ Hint Extern 1 (Register_spec val_incr) => Provide rule_incr.
(** Negation *)
Definition val_not :=
ValFun 'n := If_ val_eq 'n true Then false Else true.
ValFun 'n := If_ 'n '= true Then false Else true.
Lemma rule_not : forall (b:bool),
triple (val_not b)
......@@ -78,7 +78,7 @@ Hint Extern 1 (Register_spec val_not) => Provide rule_not.
Definition val_neq :=
ValFun 'm 'n :=
Let 'x := val_eq 'm 'n in
Let 'x := ('m '= 'n) in
val_not 'x.
Lemma rule_neq : forall v1 v2,
......@@ -301,7 +301,7 @@ Notation "'Array'' p `[ i ] `<- x" := (trm_app (trm_app (trm_app (trm_val val_ar
Definition val_array_make : val :=
ValFun 'n 'v :=
Let 'p := val_alloc 'n in
Let 'b := val_sub 'n 1 in
Let 'b := 'n '- 1 in
For 'i := 0 To 'b Do (* todo: allow inlining of B *)
Array' 'p`['i] `<- 'v
Done;;
......
......@@ -587,10 +587,167 @@ Tactic Notation "xrule_new_record" :=
(* ********************************************************************** *)
(* * Lifted access rules for arrays *)
(* TODO *)
(* ---------------------------------------------------------------------- *)
(** Representation *)
Fixpoint Array A `{EA:Enc A} (L:list A) (p:loc) : hprop :=
match L with
| nil => \[]
| x::L' => (p ~~> x) \* (Array L' (S p))
end.
(* TODO: move *)
Lemma repr_eq : forall (A:Type) (S:A->hprop) (x:A),
(x ~> S) = S x.
Proof using. auto. Qed.
Section ArrayProp.
Context A `{EA:Enc A}.
Implicit Types L : list A.
Implicit Types x : A.
Lemma Array_eq_NonLiftedArray : forall L p,
Array L p = LambdaStruct.Array (LibList.map enc L) p.
Proof using.
intros L. induction L; intros.
{ auto. }
{ simpl. rewrite IHL. rew_listx. rewrite Array_cons_eq. auto. }
Qed.
Lemma Array_unlift : forall L p,
p ~> Array L = LambdaStruct.Array (LibList.map enc L) p.
Proof using. apply Array_eq_NonLiftedArray. Qed.
(* TODO: better exploit factorization with LambdaStruct using lemma above? *)
Lemma Array_nil_eq : forall p,
p ~> Array (@nil A) = \[].
Proof using. auto. Qed.
Lemma Array_cons_eq : forall p x L,
p ~> Array (x::L) = (p ~~> x) \* (S p) ~> Array L.
Proof using. auto. Qed.
Lemma Array_one_eq : forall p x,
p ~> Array (x::nil) = (p ~~> x).
Proof using. intros. rewrite Array_cons_eq, Array_nil_eq. rew_heap~. Qed.
Lemma Array_concat_eq : forall p L1 L2,
p ~> Array (L1++L2) = p ~> Array L1 \* (p + length L1)%nat ~> Array L2.
Proof using.
intros. repeat rewrite Array_unlift. rew_listx. rewrite Array_concat_eq.
rewrite length_map. auto. (* TODO: add to rew_listx. *)
(*
Transparent loc.
intros. gen p. induction L1; intros; rew_list.
{ rewrite Array_nil_eq. rew_heap. fequals. unfold loc; math. }
{ do 2 rewrite Array_cons_eq. rewrite IHL1. rew_heap. do 3 fequals.
unfold loc; math. }
*)
Qed.
Lemma Array_last_eq : forall p x L,
p ~> Array (L&x) = p ~> Array L \* ((p + length L)%nat ~~> x).
Proof using. intros. rewrite Array_concat_eq. rewrite~ Array_one_eq. Qed.
Transparent loc. (* TODO: avoid this using pointer arithmetic operator for p+n *)
Lemma Array_middle_eq' : forall n p L,
0 <= n < length L ->
(p ~> Array L) = Hexists L1 x L2, \[L = L1++x::L2] \* \[length L1 = n :> int] \*
p ~> Array L1 \* (abs(p+n) ~~> x) \* (p + length L1 + 1)%nat ~> Array L2.
Proof using.
(* TODO: reuse proof from LambdaStruct *)
(*
introv N. applys himpl_antisym.
{ forwards (L1&x&L2&E&HM): list_middle_inv (abs n) L.
asserts (N1&N2): (0 <= abs n /\ (abs n < length L)%Z).
{ split; rewrite abs_nonneg; math. } math.
lets M': eq_int_of_eq_nat HM. rewrite abs_nonneg in M'; [|math].
hsimpl~ (>> L1 x L2). subst L. rewrite Array_concat_eq, Array_cons_eq.
rew_nat. hsimpl. rewrite HM. rewrite~ abs_nat_plus_nonneg. math. }
{ hpull ;=> L1 x L2 HM E. subst n.
subst L. rewrite Array_concat_eq, Array_cons_eq.
rew_nat. hsimpl. applys_eq himpl_refl 1. fequals.
rewrite abs_nat_plus_nonneg; [|math]. rewrite~ abs_nat. }
*)
skip.
Qed.
End ArrayProp.
Global Opaque Array.
Lemma Rule_alloc_array : forall n,
n >= 0 ->
Triple (val_alloc `n)
PRE \[]
POST (fun p => Hexists (L:list val), \[length L = n :> int] \* p ~> Array L).
Proof using.
intros. unfold Triple. xapplys~ rule_alloc_array.
intros r x L. intros E N. subst.
unfold Post. hsimpl~ L.
rewrite Array_unlift.
asserts_rewrite (@enc val _ = @id val). (* TODO: map_id extens *)
{ extens. intros v. rewrite~ enc_val_eq. }
rewrite map_id. hsimpl.
Qed.
Import LibListZ.
Implicit Types i ofs len : int.
Section ArrayRules.
Context A `{EA:Enc A} `{IA:Inhab A}.
Implicit Types L : list A.
Lemma Rule_array_get : forall p i L,
index L i ->
Triple (val_array_get `p `i)
PRE (p ~> Array L)
POST (fun (r:A) => \[r = L[i]] \* p ~> Array L).
Proof using.
intros. unfold Triple. rewrite Array_unlift.
xapplys~ rule_array_get. skip. (* todo! index_map *)
intros r E. (* todo: read_map *)
unfold Post. hsimpl.
Admitted.
Hint Extern 1 (Register_Spec val_array_get) => Provide Rule_array_get.
Lemma Rule_array_set : forall p i v L,
index L i ->
Triple (val_array_set `p `i `v)
PRE (p ~> Array L)
POST (fun (_:unit) => p ~> Array (L[i:=v])).
Proof using.
intros. unfold Triple. rewrite Array_unlift.
xapplys~ rule_array_set. skip. (* todo! index_map *)
intros r E. (* todo: update_map *)
unfold Post. hsimpl~.
Admitted.
Hint Extern 1 (Register_Spec val_array_set) => Provide Rule_array_set.
Lemma Rule_array_make : forall n v,
n >= 0 ->
Triple (val_array_make `n `v)
PRE \[]
POST (fun p => Hexists L, \[L = make n v] \* p ~> Array L).
Proof using.
intros. unfold Triple.
xapplys~ rule_array_make.
intros r p L E N. (* todo: update_map *)
unfold Post. hsimpl~ p (make n v).
rewrite Array_unlift. subst L. (* todo: map_make *)
Admitted.
Hint Extern 1 (Register_Spec val_array_make) => Provide Rule_array_make.
End ArrayRules.
......
......@@ -142,3 +142,11 @@ Tactic Notation "isubst" :=
isbust_core tt.
(*----------------------*)
(* LibInt *)
Global Opaque Z.mul.
Global Opaque Z.add.
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