Commit 0062010f authored by charguer's avatar charguer

new_record

parent 33801ca2
(* TODO DEPRECATED
Definition nats := list nat.
Fixpoint nat_fresh (y:nat) (xs:nats) : bool :=
match xs with
| nil => true
| x::xs' => if eq_nat_dec x y then false else nat_fresh y xs'
end.
Fixpoint nat_distinct (xs:nats) : bool :=
match xs with
| nil => true
| x::xs' => nat_fresh x xs' && nat_distinct xs'
end.
(** [nat_seq i n] generates a list of variables [x1;x2;..;xn]
with [x1=i] and [xn=i+n-1]. Such lists are useful for
generic programming. *)
Fixpoint nat_seq (start:nat) (nb:nat) :=
match nb with
| O => nil
| S nb' => start :: nat_seq (S start) nb'
end.
Section Nat_seq.
Implicit Types start nb : nat.
Lemma var_fresh_nat_seq_lt : forall x start nb,
(x < start)%nat ->
nat_fresh x (nat_seq start nb).
Proof using.
intros. gen start. induction nb; intros.
{ auto. }
{ simpl. case_if. { math. } { applys IHnb. math. } }
Qed.
Lemma var_fresh_nat_seq_ge : forall x start nb,
(x >= start+nb)%nat ->
nat_fresh x (nat_seq start nb).
Proof using.
intros. gen start. induction nb; intros.
{ auto. }
{ simpl. case_if. { math. } { applys IHnb. math. } }
Qed.
Lemma var_distinct_nat_seq : forall start nb,
nat_distinct (nat_seq start nb).
Proof using.
intros. gen start. induction nb; intros.
{ auto. }
{ simpl. rew_istrue. split.
{ applys var_fresh_nat_seq_lt. math. }
{ auto. } }
Qed.
Lemma length_nat_seq : forall start nb,
length (nat_seq start nb) = nb.
Proof using.
intros. gen start. induction nb; simpl; intros.
{ auto. } { rew_list. rewrite~ IHnb. }
Qed.
(* TODO: convert nat to var
Lemma var_funs_nat_seq : forall start nb,
(nb > 0%nat)%nat ->
var_funs nb (nat_seq start nb).
Proof using.
introv E. splits.
{ applys var_distinct_nat_seq. }
{ applys length_nat_seq. }
{ destruct nb. { false. math. } { simpl. auto_false. } }
Qed.
*)
End Nat_seq.
*)
\ No newline at end of file
......@@ -594,6 +594,7 @@ Tactic Notation "rew_vals_to_trms" :=
(** Distinct variables *)
(* TODO: use LibListExec *)
(* TODO: generalize to lists *)
Fixpoint var_fresh (y:var) (xs:vars) : bool :=
match xs with
......@@ -870,83 +871,89 @@ Proof using. intros. rew_nary. Abort.
(* ---------------------------------------------------------------------- *)
(* ** Sequence of consecutive variables *)
(* TODO: generalize to lists *)
(** [nat_to_var n] converts [nat] values into distinct
[var] values.
Warning: the current implementation is inefficient. *)
Definition nats := list nat.
Definition dummy_char := Ascii.ascii_of_nat 0%nat.
Fixpoint nat_fresh (y:nat) (xs:nats) : bool :=
match xs with
| nil => true
| x::xs' => if eq_nat_dec x y then false else nat_fresh y xs'
Fixpoint nat_to_var (n:nat) : var :=
match n with
| O => String.EmptyString
| S n' => String.String dummy_char (nat_to_var n')
end.
Fixpoint nat_distinct (xs:nats) : bool :=
match xs with
| nil => true
| x::xs' => nat_fresh x xs' && nat_distinct xs'
end.
Lemma injective_nat_to_var : injective nat_to_var.
Proof using.
intros n. induction n as [|n']; intros m E; destruct m as [|m']; tryfalse.
{ auto. }
{ inverts E. fequals~. }
Qed.
(** [nat_seq i n] generates a list of variables [x1;x2;..;xn]
(** [var_seq i n] generates a list of variables [x1;x2;..;xn]
with [x1=i] and [xn=i+n-1]. Such lists are useful for
generic programming. *)
Fixpoint nat_seq (start:nat) (nb:nat) :=
Fixpoint var_seq (start:nat) (nb:nat) : vars :=
match nb with
| O => nil
| S nb' => start :: nat_seq (S start) nb'
| S nb' => (nat_to_var start) :: var_seq (S start) nb'
end.
Section Nat_seq.
Section Var_seq.
Implicit Types start nb : nat.
Lemma var_fresh_nat_seq_lt : forall x start nb,
Lemma var_fresh_var_seq_lt : forall x start nb,
(x < start)%nat ->
nat_fresh x (nat_seq start nb).
var_fresh (nat_to_var x) (var_seq start nb).
Proof using.
intros. gen start. induction nb; intros.
{ auto. }
{ simpl. case_if. { math. } { applys IHnb. math. } }
{ simpl. case_if.
{ lets: injective_nat_to_var C. math. }
{ applys IHnb. math. } }
Qed.
Lemma var_fresh_nat_seq_ge : forall x start nb,
Lemma var_fresh_var_seq_ge : forall x start nb,
(x >= start+nb)%nat ->
nat_fresh x (nat_seq start nb).
var_fresh (nat_to_var x) (var_seq start nb).
Proof using.
intros. gen start. induction nb; intros.
{ auto. }
{ simpl. case_if. { math. } { applys IHnb. math. } }
{ simpl. case_if.
{ lets: injective_nat_to_var C. math. }
{ applys IHnb. math. } }
Qed.
Lemma var_distinct_nat_seq : forall start nb,
nat_distinct (nat_seq start nb).
Lemma var_distinct_var_seq : forall start nb,
var_distinct (var_seq start nb).
Proof using.
intros. gen start. induction nb; intros.
{ auto. }
{ simpl. rew_istrue. split.
{ applys var_fresh_nat_seq_lt. math. }
{ applys var_fresh_var_seq_lt. math. }
{ auto. } }
Qed.
Lemma length_nat_seq : forall start nb,
length (nat_seq start nb) = nb.
Lemma length_var_seq : forall start nb,
length (var_seq start nb) = nb.
Proof using.
intros. gen start. induction nb; simpl; intros.
{ auto. } { rew_list. rewrite~ IHnb. }
Qed.
(* TODO: convert nat to var
Lemma var_funs_nat_seq : forall start nb,
Lemma var_funs_var_seq : forall start nb,
(nb > 0%nat)%nat ->
var_funs nb (nat_seq start nb).
var_funs nb (var_seq start nb).
Proof using.
introv E. splits.
{ applys var_distinct_nat_seq. }
{ applys length_nat_seq. }
{ applys var_distinct_var_seq. }
{ applys length_var_seq. }
{ destruct nb. { false. math. } { simpl. auto_false. } }
Qed.
*)
End Nat_seq.
End Var_seq.
(* ********************************************************************** *)
......
......@@ -398,6 +398,32 @@ Ltac xspec_base tt ::=
end.
(* ---------------------------------------------------------------------- *)
(* ** *)
(* TODO :move *)
(** [nat_seq i n] generates a list of variables [x1;x2;..;xn]
with [x1=i] and [xn=i+n-1]. Such lists are useful for
generic programming. *)
(* TODO: move to LibNat *)
Fixpoint nat_seq (start:nat) (nb:nat) :=
match nb with
| O => nil
| S nb' => start :: nat_seq (S start) nb'
end.
Lemma length_nat_seq : forall start nb,
length (nat_seq start nb) = nb.
Proof using.
intros. gen start. induction nb; simpl; intros.
{ auto. } { rew_list. rewrite~ IHnb. }
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Conversion between allocated segments and record representation *)
......@@ -466,25 +492,27 @@ Qed.
(* ---------------------------------------------------------------------- *)
(* ** Specification for allocation of records of arbitrary arity *)
(* TODO: convert nat to var
Definition val_new_record (n:nat) :=
let xs := nat_seq 0%nat n in
let P : var := n%nat in
let fs := nat_seq 0%nat n in
let xs := var_seq 0%nat n in
let P : var := nat_to_var n in
val_funs xs (
Let P := val_alloc n in
LibList.fold_right (fun x t => val_set_field (x:field) P (x:var);; t) (trm_var P) xs).
LibList.fold_right (fun f t => val_set_field (f:field) P (nat_to_var f);; t) (trm_var P) fs).
Lemma Subst_new_record_aux : forall xs Vs (i n n':nat) (p:loc),
Lemma Subst_new_record_aux : forall fs xs Vs (i n n':nat) (p:loc),
n' = length Vs ->
xs = nat_seq i n' ->
fs = nat_seq i n' ->
xs = var_seq i n' ->
(i + n' = n)%nat ->
(Subst n (Dyn p) (Substs xs Vs (fold_right (fun x t => trm_seq (val_set_field x (trm_var n) (trm_var x)) t) (trm_var n) xs)))
= fold_right (fun xV t => let '(x,V) := xV in trm_seq (val_set_field x p (enc V)) t) p (LibList.combine xs Vs).
let N := nat_to_var n in
(Subst N (Dyn p) (Substs xs Vs (fold_right (fun f t => trm_seq (val_set_field (f:field) (trm_var N) (nat_to_var f)) t) (trm_var N) fs)))
= fold_right (fun fV t => let '(f,V) := fV in trm_seq (val_set_field (f:field) p (enc V)) t) p (LibList.combine fs Vs).
Proof using.
(*
intros xs. induction xs as [|x xs']; introv LVs Exs Ein.
{ simpl combine. rew_list. unfold Subst. simpl. case_if~. }
{ forwards Lin: length_nat_seq i n'.
{ forwards Lin: length_var_seq i n'.
rewrite <- Exs in Lin. rew_list in Lin.
destruct Vs as [|V Vs']. { false. rew_list in LVs. math. }
rew_list in LVs. asserts EL: (length xs' = length Vs'). { math. }
......@@ -500,7 +528,7 @@ Proof using.
asserts_rewrite (Substs xs' Vs' (val_set_field x (trm_var n) `V)
= (val_set_field x (trm_var n) `V)).
{ do 2 rewrite~ Substs_app. do 2 rewrite~ Substs_val. rewrite~ Substs_var_neq.
{ rewrite Exs'. applys var_fresh_nat_seq_ge. math. } }
{ rewrite Exs'. applys var_fresh_var_seq_ge. math. } }
rewrite~ Subst_seq.
asserts_rewrite (Subst n (Dyn p) (val_set_field x (trm_var n) `V) = val_set_field x p `V).
{ unfold Subst; simpl. case_if~. } (* todo: lemma Subst_var *)
......@@ -509,7 +537,7 @@ Proof using.
asserts_rewrite (Subst x V t = t).
{ subst xs'. cuts K: (forall n' i,
(x < i)%nat ->
let t := @fold_right nat trm (fun f t => trm_seq (val_set_field f (trm_var n) (trm_var f)) t) (trm_var n) (nat_seq i n') in
let t := @fold_right nat trm (fun f t => trm_seq (val_set_field f (trm_var n) (trm_var f)) t) (trm_var n) (var_seq i n') in
Subst x V t = t).
{ applys K. math. }
intros n'. gen N. clears_all. induction n'; introv L; intros; subst t.
......@@ -518,49 +546,57 @@ Proof using.
{ unfold Subst. simpl. case_if. case_if. { false; math. } { auto. } }
{ rewrite~ IHn'. } } }
applys IHxs' Exs'; math. }
*)
admit.
Qed.
Lemma Rule_new_record : forall (n:nat) (Vs:dyns),
(n > 0)%nat ->
n = length Vs ->
let xs := nat_seq 0%nat n in
let fs := nat_seq 0%nat n in
let xs := var_seq 0%nat n in
Triple (trm_apps (val_new_record n) (encs Vs))
PRE \[]
POST (fun p => p ~> Record (combine xs Vs)).
POST (fun p => p ~> Record (combine fs Vs)).
Proof using.
introv HP LVs. intros xs. applys Rule_apps_funs.
introv HP LVs. intros fs xs. applys Rule_apps_funs.
{ reflexivity. }
{ subst. applys~ var_funs_nat_seq. }
{ asserts EL: (length Vs = length xs). { unfold xs. rewrite~ length_nat_seq. }
rewrite Substs_let; [| applys var_fresh_nat_seq_ge; math | auto ].
asserts_rewrite (Substs (nat_seq 0 n) Vs (val_alloc n) = val_alloc n).
{ rewrite~ Substs_app. do 2 rewrite~ Substs_val. }
{ subst. applys~ var_funs_var_seq. }
{ asserts EL: (length Vs = length xs). { unfold xs. rewrite~ length_var_seq. }
rewrite Substs_let; [| applys var_fresh_var_seq_ge; math | auto ].
asserts_rewrite (Substs (var_seq 0 n) Vs (val_alloc n) = val_alloc n).
{ rewrite~ Substs_app. rewrite~ Substs_val. do 2 rewrite~ Substs_val. }
eapply (@Rule_let _ _ _ _ _ _ _ loc). (* todo: cleanup *)
{ xapplys Rule_alloc_nat. }
{ intros p. xpull ;=> Np. xchange~ (@Alloc_to_Record p 0%nat).
{ math_rewrite ((p+0)%nat = p). hsimpl. } (* todo simplify *)
xpull ;=> Ws LWs. fold xs.
rewrite (@Subst_new_record_aux xs Vs 0%nat n n); try first [ math | auto ].
asserts Lxs: (length xs = n). { subst xs. rewrite~ length_nat_seq. }
clearbody xs. clear HP.
applys local_weaken_post (fun p' => \[p' = p] \* p ~> Record (combine xs Vs));
[ xlocal | | hsimpl; intros; subst~]. (* todo: weaken_post with swapped order *)
gen n Vs Ws. induction xs; intros.
{ simpl. (* todo: rew_list *) applys~ Rule_val p. hsimpl~. }
{ rew_list in Lxs.
destruct Vs as [|V Vs']; rew_list in LVs.
{ false; math. }
destruct Ws as [|W Ws']; rew_list in LWs.
{ false; math. }
destruct n as [|n']. { false; math. }
{ do 2 rewrite combine_cons. rew_list.
xpull ;=> Ws LWs. fold xs. fold fs.
rewrite (@Subst_new_record_aux fs xs Vs 0%nat n n); try first [ math | auto ].
asserts Lxs: (length xs = n). { subst xs. rewrite~ length_var_seq. }
(*clearbody xs.*) clear HP.
applys local_weaken_post (fun p' => \[p' = p] \* p ~> Record (combine fs Vs));
[ xlocal | | hsimpl; intros; subst~]. (* todo: weaken_post with swapped order *)
gen n Vs Ws. set (start := O). intros n. gen start.
induction n as [|n']; intros.
{ destruct xs; [|rew_list in *; false; math].
destruct Vs; [|rew_list in *; false; math].
destruct Ws; [|rew_list in *; false; math].
rew_list in *. subst. simpls.
applys~ Rule_val p. hsimpl~. }
{ destruct xs as [|xs']; [rew_list in *; false; math|].
destruct Vs as [|V Vs']; [rew_list in *; false; math|].
destruct Ws as [|W Ws'] ; [rew_list in *; false; math|].
rew_list in *. simpl in fs. subst fs.
do 2 rewrite combine_cons. rew_listx.
rewrite Record_cons. applys Rule_seq.
{ xapplys @Rule_set_field. }
{ simpl. xapply (>> IHxs n' Vs' Ws'); try math.
{ hsimpl. } { intros p'. rewrite Record_cons. hsimpl~. } } } } } }
{ simpl. lets M: (>> IHn' (S start) Vs' Ws' __);
try rewrite length_var_seq; try math.
xapply M. { hsimpl. }
{ intros p'. rewrite Record_cons. hsimpl~. } } } } }
Qed.
*)
(*
Parameter val_new_record : nat -> val.
......@@ -571,15 +607,15 @@ Parameter Rule_new_record : forall (n:nat) (Vs:dyns),
Triple (trm_apps (val_new_record n) (encs Vs))
PRE \[]
POST (fun p => p ~> Record (combine xs Vs)).
*)
Lemma Rule_new_record' : forall (n:nat) (Vs:dyns) (vs:vals) (Q:loc->hprop),
vs = (encs Vs) ->
(n = List.length Vs)%nat ->
(n > 0)%nat ->
let xs := nat_seq 0%nat n in
((fun p => p ~> Record (List.combine xs Vs)) ===> Q) ->
let fs := nat_seq 0%nat n in
let xs := var_seq 0%nat n in
((fun p => p ~> Record (List.combine fs Vs)) ===> Q) ->
Triple (trm_apps (val_new_record n) (vals_to_trms vs)) \[] Q.
Proof using.
introv E HL HP HQ. rewrite List_length_eq in HL.
......@@ -589,8 +625,8 @@ Qed.
(** Tactic [xrule_new_record] for proving the specification
triple for the allocation of a specific record.
For an example, check out [ExampleTree.v],
Definition [val_new_node] and Lemma [Rule_new_node]. *)
For an example, check out in [ExampleTree.v],
Definition [val_new_node] and Lemma [Rule_new_node]. *)
Ltac xrule_new_record_core tt :=
intros; rew_nary; rew_vals_to_trms; applys Rule_new_record';
......
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