Commit 61213d3d authored by charguer's avatar charguer

array

parent bd90597a
......@@ -2835,7 +2835,7 @@ Ltac xcf_core_spec f :=
intros [C H];
split;
[ clear H; try apply C (* curried part *)
| clear C; xcf_core_app_exploit H ].
| clear C; intros; xcf_core_app_exploit H ].
Ltac xcf_core_app f :=
xcf_find f;
......@@ -2860,6 +2860,7 @@ Ltac xcf_core tt :=
intros;
match goal with
| |- spec ?f ?n ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- curried ?n ?f /\ ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- app ?f ?xs ?H ?Q => first [ xcf_core_app f | xcf_fallback f | fail 2 ]
| |- tag tag_apply (app ?f ?xs ?H ?Q) => first [ xuntag tag_apply; xcf_core_app f | xcf_fallback f | fail 2 ]
| |- ?f = _ => first [ xcf_top_value f | xcf_fallback f | fail 2 ]
......@@ -2992,3 +2993,46 @@ Ltac xskip_credits_base :=
Tactic Notation "xskip_credits" :=
xskip_credits_base.
(********************************************************************)
(* ** Tactics for Automation *)
Ltac xgo_step tt :=
match cfml_get_tag tt with
| tag_ret => xret
| tag_apply => xapp
| tag_val => xval
| tag_fun => xfun
| tag_let => xlet
| tag_match => xmatch
| tag_case => xcase
| tag_fail => xfail
| tag_done => xdone
| tag_alias => xalias
| tag_seq => xseq
| tag_if => xif
| tag_for => fail 1
| tag_while => fail 1
| tag_assert => fail 1 (* TODO assert *)
| _ =>
match goal with
| |- _ ==> _ => first [ xsimpl | fail 2 ]
| |- _ ===> _ => first [ xsimpl | fail 2 ]
end
end.
(*
| tag_casewhen => fail 1
| tag_app_curried
| tag_pay*)
Ltac xgo_core tt :=
repeat (try (xextract; intros); xgo_step tt; instantiate).
Tactic Notation "xgo" :=
xgo_core tt.
Tactic Notation "xgo" "~" :=
xgo; xauto~.
Tactic Notation "xgo" "*" :=
xgo; xauto*.
Set Implicit Arguments.
Require Import CFLib.
Require Import Pervasives_ml Pervasives_proof.
Require Export LibListZ.
Require Import Array_ml.
Generalizable Variables A.
(************************************************************)
(** Arrays *)
(** Builtin *)
(** The model of an imperative array is a sequence, represented as a list *)
Parameter Array : forall A (L:list A) (l:loc), hprop.
Definition array (A:Type) := list A.
Parameter make_from_list_spec : curried 2%nat make_from_list /\
forall A (L:list A),
app make_from_list [L] \[] (fun t => t ~> Array L).
Parameter ArrayOf : forall a A (T:htype A a) (M:array A) (l:loc), hprop.
Hint Extern 1 (RegisterSpec make_from_list) => Provide make_from_list_spec.
Notation "'Array'" := (ArrayOf Id).
Require Import LibBag.
Lemma make_empty_spec : forall A,
app make_empty [tt] \[] (fun l => l ~> Array (@nil A)).
Proof using.
xcf. xgo.
Qed.
Parameter caml_array_make_spec : forall a,
Spec caml_array_make (n:int) (v:a) |R>>
n >= 0 ->
R \[] (fun l => Hexists M, l ~> Array M \* \[M = make n v]).
(* Note: zmake is the make function for lists with an argument in Z *)
Hint Extern 1 (RegisterSpec make_empty) => Provide make_empty_spec.
Parameter make_spec : curried 2%nat make /\
forall A (n:int) (v:A),
n >= 0 ->
app make [n v] \[] (fun t =>
Hexists L, t ~> Array L \* \[L = LibListZ.make n v]).
Hint Extern 1 (RegisterSpec make) => Provide make_spec.
Lemma make_spec_direct : forall A (n:int) (v:A),
n >= 0 ->
app make [n v] \[] (fun l => l ~> Array (LibListZ.make n v)).
Proof using.
intros. xapp~. xsimpl~.
Qed.
Parameter length_spec : curried 1%nat length /\
forall A (L:list A) (t:loc),
app_keep length [t] (t ~> Array L) (fun n => \[n = LibList.length L]).
Hint Extern 1 (RegisterSpec length) => Provide length_spec.
Parameter get_spec : curried 2%nat get /\
forall `{Inhab A} (L:list A) (t:loc) (i:int),
index L i ->
app_keep get [t i] (t ~> Array L) \[= L[i] ].
Hint Extern 1 (RegisterSpec get) => Provide get_spec.
Parameter caml_array_make_spec_direct : forall a,
Spec caml_array_make (n:int) (v:a) |R>>
R \[] (fun l => l ~> Array (make n v)).
(* todo: prove as a derived lemma *)
Parameter set_spec : curried 2%nat set /\
forall A (L:list A) (t:loc) (i:int) (v:A),
index L i ->
app set [t i v] (t ~> Array L) (# t ~> Array (L[i:=v])).
Hint Extern 1 (RegisterSpec get) => Provide get_spec.
Parameter caml_array_get_spec : forall a,
Spec caml_array_get (l:loc) (i:int) |R>>
forall `{Inhab a} (t:list a), index t i ->
keep R (l ~> Array t) (fun x => \[x = t[i]]).
Parameter caml_array_set_spec : forall a,
Spec caml_array_set (l:loc) (i:int) (v:a) |R>>
forall (t:list a), index t i ->
R (l ~> Array t) (# l ~> Array (t[i:=v])).
Parameter caml_array_length_spec : forall a,
Spec caml_array_length (l:loc) |R>> forall (t:array a),
keep R (l ~> Array t) (fun x => \[x = length t]).
Hint Extern 1 (RegisterSpec caml_array_make) => Provide caml_array_make_spec.
Hint Extern 1 (RegisterSpec caml_array_get) => Provide caml_array_get_spec.
Hint Extern 1 (RegisterSpec caml_array_set) => Provide caml_array_set_spec.
Hint Extern 1 (RegisterSpec caml_array_length) => Provide caml_array_length_spec.
(************************************************************)
(************************************************************)
(************************************************************)
(** FUTURE
(** The model of an imperative array is a sequence, represented as a list *)
Definition array (A:Type) := list A.
Parameter ArrayOf : forall a A (T:htype A a) (M:array A) (l:loc), hprop.
Notation "'Array'" := (ArrayOf Id).
Require Import LibBag.
(* -- with credits ---*)
......@@ -63,3 +104,4 @@ Parameter ml_array_make_spec : forall a,
Hint Extern 1 (RegisterSpecCredits ml_array_make) => Provide ml_array_make_spec.
*)
\ No newline at end of file
......@@ -4,70 +4,6 @@ Require Import Pervasives_ml.
Ltac xgo_step tt :=
match cfml_get_tag tt with
| tag_ret => xret
| tag_apply => xapp
| tag_val => xval
| tag_fun => xfun
| tag_let => xlet
| tag_match => xmatch
| tag_case => xcase
| tag_fail => xfail
| tag_done => xdone
| tag_alias => xalias
| tag_seq => xseq
| tag_if => xif
| tag_for => fail 1
| tag_while => fail 1
| tag_assert => fail 1 (* TODO assert *)
| _ =>
match goal with
| |- _ ==> _ => first [ xsimpl | fail 2 ]
| |- _ ===> _ => first [ xsimpl | fail 2 ]
end
end.
(*
| tag_casewhen => fail 1
| tag_app_curried
| tag_pay*)
Ltac xgo_core tt :=
repeat (try (xextract; intros); xgo_step tt; instantiate).
Tactic Notation "xgo" :=
xgo_core tt.
Tactic Notation "xgo" "~" :=
xgo; xauto~.
Tactic Notation "xgo" "*" :=
xgo; xauto*.
Ltac xcf_core tt ::=
intros;
match goal with
| |- spec ?f ?n ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- curried ?n ?f /\ ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- app ?f ?xs ?H ?Q => first [ xcf_core_app f | xcf_fallback f | fail 2 ]
| |- tag tag_apply (app ?f ?xs ?H ?Q) => first [ xuntag tag_apply; xcf_core_app f | xcf_fallback f | fail 2 ]
| |- ?f = _ => first [ xcf_top_value f | xcf_fallback f | fail 2 ]
| _ => fail 1 "need to call [xcf f; => H], where [f] is the name of the definition"
end.
Ltac xcf_core_spec f ::=
xcf_find f;
let C := fresh "Curried" in
let H := fresh "Spec" in
intros [C H];
split;
[ clear H; try apply C (* curried part *)
| clear C; intros; xcf_core_app_exploit H ].
(************************************************************)
(** Boolean *)
......@@ -122,9 +58,7 @@ Parameter neq_int_spec : neq_spec_for int.
Hint Extern 1 (RegisterSpec infix_lt_gt_) => Provide neq_int_spec.
(* LATER: give specification for partially applied comparison operators *)
(* LATER: give specification for partially applied comparison operators *)
Lemma min_spec : forall (n m:int),
app min [n m] \[] \[= Coq.ZArith.BinInt.Zmin n m ].
......@@ -239,26 +173,26 @@ Hint Extern 1 (RegisterSpec abs) => Provide abs_spec.
(************************************************************)
(** References *)
Definition Ref a (v:a) (l:loc) := (* TODO: change *)
heap_is_single l v.
Definition Ref a (v:a) (r:loc) := (* TODO: change *)
heap_is_single r v.
Notation "l '~~>' v" := (hdata (Ref v) l)
Notation "r '~~>' v" := (hdata (Ref v) r)
(at level 32, no associativity) : heap_scope.
Lemma ref_spec : forall a (v:a),
app ref [v] \[] (fun l => l ~~> v).
app ref [v] \[] (fun r => r ~~> v).
Proof using.
xcf. skip.
Qed.
Lemma infix_emark__spec : forall a (v:a) l,
app_keep infix_emark_ [l] (l ~~> v) \[= v].
Lemma infix_emark__spec : forall a (v:a) r,
app_keep infix_emark_ [r] (r ~~> v) \[= v].
Proof using.
xcf. skip.
Qed.
Lemma infix_colon_eq__spec : forall a (v w:a) l,
app infix_colon_eq_ [l w] (l ~~> v) (# l ~~> w).
Lemma infix_colon_eq__spec : forall a (v w:a) r,
app infix_colon_eq_ [r w] (r ~~> v) (# r ~~> w).
Proof using.
xcf. skip.
Qed.
......@@ -267,14 +201,14 @@ Hint Extern 1 (RegisterSpec ref) => Provide ref_spec.
Hint Extern 1 (RegisterSpec infix_emark_) => Provide infix_emark__spec.
Hint Extern 1 (RegisterSpec infix_colon_eq_) => Provide infix_colon_eq__spec.
Lemma incr_spec : forall (n:int) l,
app incr [l] (l ~~> n) (# l ~~> (n+1)).
Lemma incr_spec : forall (n:int) r,
app incr [r] (r ~~> n) (# r ~~> (n+1)).
Proof using.
xcf. xgo~.
Qed.
Lemma decr_spec : forall (n:int) l,
app decr [l] (l ~~> n) (# l ~~> (n-1)).
Lemma decr_spec : forall (n:int) r,
app decr [r] (r ~~> n) (# r ~~> (n-1)).
Proof using.
xcf. xgo~.
Qed.
......@@ -341,8 +275,8 @@ Hint Extern 1 (RegisterSpec ignore) => Provide ignore_spec.
(*------------------------------------------------------------------*)
(* ** References *)
Definition Ref a A (T:htype A a) (V:A) (l:loc) :=
Hexists v, heap_is_single l v \* v ~> T V.
Definition Ref a A (T:htype A a) (V:A) (r:loc) :=
Hexists v, heap_is_single r v \* v ~> T V.
Instance Ref_Heapdata : forall a A (T:htype A a),
(Heapdata (@Ref a A T)).
......@@ -358,22 +292,22 @@ Notation "'~~>' v" := (~> Ref (@Id _) v)
(at level 32, no associativity) : heap_scope_advanced.
(*
Notation "l '~~>' v" := (l ~> Ref (@Id _) v)
Notation "l '~~>' v" := (r ~> Ref (@Id _) v)
(at level 32, no associativity) : heap_scope.
*)
Notation "l '~~>' v" := (hdata (@Ref _ _ (@Id _) v) l)
Notation "l '~~>' v" := (hdata (@Ref _ _ (@Id _) v) r)
(at level 32, no associativity) : heap_scope.
Lemma focus_ref : forall (l:loc) a A (T:htype A a) V,
l ~> Ref T V ==> Hexists v, l ~~> v \* v ~> T V.
Lemma focus_ref : forall (r:loc) a A (T:htype A a) V,
r ~> Ref T V ==> Hexists v, r ~~> v \* v ~> T V.
Proof. intros. unfold Ref, hdata. unfold Id. hsimpl~. Qed.
Lemma unfocus_ref : forall (l:loc) a (v:a) A (T:htype A a) V,
l ~~> v \* v ~> T V ==> l ~> Ref T V.
Lemma unfocus_ref : forall (r:loc) a (v:a) A (T:htype A a) V,
r ~~> v \* v ~> T V ==> r ~> Ref T V.
Proof. intros. unfold Ref. hdata_simpl. hsimpl. subst~. Qed.
Lemma heap_is_single_impl_null : forall (l:loc) A (v:A),
heap_is_single l v ==> heap_is_single l v \* \[l <> null].
Lemma heap_is_single_impl_null : forall (r:loc) A (v:A),
heap_is_single r v ==> heap_is_single r v \* \[r <> null].
Proof.
intros. intros h Hh. forwards*: heap_is_single_null. exists___*.
Qed.
......@@ -397,27 +331,27 @@ Implicit Arguments unfocus_ref [a A].
Parameter caml_ref_spec_group : forall a,
Spec caml_ref (v:a) |R>> forall (M:map loc a),
R (Group (Ref Id) M) (fun (l:loc) =>
Group (Ref Id) (M[l:=v]) \* \[l \notindom M]).
R (Group (Ref Id) M) (fun (r:loc) =>
Group (Ref Id) (M[r:=v]) \* \[r \notindom M]).
Lemma caml_get_spec_group : forall a,
Spec caml_get (l:loc) |R>> forall (M:map loc a),
forall `{Inhab a}, l \indom M ->
keep R (Group (Ref Id) M) (fun x => \[x = M[l]]).
Spec caml_get (r:loc) |R>> forall (M:map loc a),
forall `{Inhab a}, r \indom M ->
keep R (Group (Ref Id) M) (fun x => \[x = M[r]]).
Proof.
intros. xweaken. intros l R LR HR M IA IlM. simpls.
rewrite~ (Group_rem l M). xapply (HR (M[l])); hsimpl~.
intros. xweaken. intros r R LR HR M IA IlM. simpls.
rewrite~ (Group_rem r M). xapply (HR (M[r])); hsimpl~.
Qed.
Lemma caml_set_spec_group : forall a,
Spec caml_set (l:loc) (v:a) |R>> forall (M:map loc a),
forall `{Inhab a}, l \indom M ->
R (Group (Ref Id) M) (# Group (Ref Id) (M[l:=v])).
Spec caml_set (r:loc) (v:a) |R>> forall (M:map loc a),
forall `{Inhab a}, r \indom M ->
R (Group (Ref Id) M) (# Group (Ref Id) (M[r:=v])).
Proof.
intros. xweaken. intros l v R LR HR M IA IlM. simpls.
rewrite~ (Group_rem l M).
xapply (HR (M[l])). hsimpl.
intros _. hchanges~ (Group_add' l M).
intros. xweaken. intros r v R LR HR M IA IlM. simpls.
rewrite~ (Group_rem r M).
xapply (HR (M[r])). hsimpl.
intros _. hchanges~ (Group_add' r M).
Qed.
......
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