summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-08-27 09:50:29 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-08-27 09:50:29 +0000
commit1abecb7b559c5e0eab8c093a629fd8197f57205f (patch)
treed506e467f81140d495967b6ca6b7125fe90df70b /lib
parenta68a6ba072bbc5d6496f6a564c4564b911efe3e8 (diff)
More efficient implementations of map, fold, etc.
(Contributed by Vincent Laporte.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2618 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib')
-rw-r--r--lib/Maps.v273
1 files changed, 109 insertions, 164 deletions
diff --git a/lib/Maps.v b/lib/Maps.v
index 3574ee2..16e3503 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -429,73 +429,62 @@ Module PTree <: TREE.
End BOOLEAN_EQUALITY.
- Fixpoint append (i j : positive) {struct i} : positive :=
- match i with
+ Fixpoint prev_append (i j: positive) {struct i} : positive :=
+ match i with
| xH => j
- | xI ii => xI (append ii j)
- | xO ii => xO (append ii j)
- end.
-
- Lemma append_assoc_0 : forall (i j : positive),
- append i (xO j) = append (append i (xO xH)) j.
- Proof.
- induction i; intros; destruct j; simpl;
- try rewrite (IHi (xI j));
- try rewrite (IHi (xO j));
- try rewrite <- (IHi xH);
- auto.
- Qed.
+ | xI i' => prev_append i' (xI j)
+ | xO i' => prev_append i' (xO j)
+ end.
- Lemma append_assoc_1 : forall (i j : positive),
- append i (xI j) = append (append i (xI xH)) j.
- Proof.
- induction i; intros; destruct j; simpl;
- try rewrite (IHi (xI j));
- try rewrite (IHi (xO j));
- try rewrite <- (IHi xH);
- auto.
- Qed.
+ Definition prev (i: positive) : positive :=
+ prev_append i xH.
- Lemma append_neutral_r : forall (i : positive), append i xH = i.
- Proof.
- induction i; simpl; congruence.
- Qed.
+ Lemma prev_append_prev i j:
+ prev (prev_append i j) = prev_append j i.
+ Proof.
+ revert j. unfold prev.
+ induction i as [i IH|i IH|]. 3: reflexivity.
+ intros j. simpl. rewrite IH. reflexivity.
+ intros j. simpl. rewrite IH. reflexivity.
+ Qed.
+
+ Lemma prev_involutive i :
+ prev (prev i) = i.
+ Proof (prev_append_prev i xH).
- Lemma append_neutral_l : forall (i : positive), append xH i = i.
- Proof.
- simpl; auto.
- Qed.
+ Lemma prev_append_inj i j j' :
+ prev_append i j = prev_append i j' -> j = j'.
+ Proof.
+ revert j j'.
+ induction i as [i Hi|i Hi|]; intros j j' H; auto;
+ specialize (Hi _ _ H); congruence.
+ Qed.
Fixpoint xmap (A B : Type) (f : positive -> A -> B) (m : t A) (i : positive)
{struct m} : t B :=
match m with
| Leaf => Leaf
- | Node l o r => Node (xmap f l (append i (xO xH)))
- (option_map (f i) o)
- (xmap f r (append i (xI xH)))
+ | Node l o r => Node (xmap f l (xO i))
+ (match o with None => None | Some x => Some (f (prev i) x) end)
+ (xmap f r (xI i))
end.
Definition map (A B : Type) (f : positive -> A -> B) m := xmap f m xH.
Lemma xgmap:
forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A),
- get i (xmap f m j) = option_map (f (append j i)) (get i m).
+ get i (xmap f m j) = option_map (f (prev (prev_append i j))) (get i m).
Proof.
induction i; intros; destruct m; simpl; auto.
- rewrite (append_assoc_1 j i); apply IHi.
- rewrite (append_assoc_0 j i); apply IHi.
- rewrite (append_neutral_r j); auto.
Qed.
Theorem gmap:
forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A),
get i (map f m) = option_map (f i) (get i m).
Proof.
- intros.
+ intros A B f i m.
unfold map.
- replace (f i) with (f (append xH i)).
- apply xgmap.
- rewrite append_neutral_l; auto.
+ rewrite xgmap. repeat f_equal. exact (prev_involutive i).
Qed.
Fixpoint map1 (A B: Type) (f: A -> B) (m: t A) {struct m} : t B :=
@@ -639,10 +628,10 @@ Module PTree <: TREE.
match m with
| Leaf => k
| Node l None r =>
- xelements l (append i (xO xH)) (xelements r (append i (xI xH)) k)
+ xelements l (xO i) (xelements r (xI i) k)
| Node l (Some x) r =>
- xelements l (append i (xO xH))
- ((i, x) :: xelements r (append i (xI xH)) k)
+ xelements l (xO i)
+ ((prev i, x) :: xelements r (xI i) k)
end.
@@ -661,16 +650,16 @@ Module PTree <: TREE.
Lemma xelements_correct:
forall (A: Type) (m: t A) (i j : positive) (v: A) k,
- get i m = Some v -> In (append j i, v) (xelements m j k).
+ get i m = Some v -> In (prev (prev_append i j), v) (xelements m j k).
Proof.
induction m; intros.
rewrite (gleaf A i) in H; congruence.
destruct o; destruct i; simpl; simpl in H.
- rewrite append_assoc_1. apply xelements_incl. right. auto.
- rewrite append_assoc_0. auto.
- inv H. apply xelements_incl. left. rewrite append_neutral_r; auto.
- rewrite append_assoc_1. apply xelements_incl. auto.
- rewrite append_assoc_0. auto.
+ apply xelements_incl. right. auto.
+ auto.
+ inv H. apply xelements_incl. left. reflexivity.
+ apply xelements_incl. auto.
+ auto.
inv H.
Qed.
@@ -679,88 +668,47 @@ Module PTree <: TREE.
get i m = Some v -> In (i, v) (elements m).
Proof.
intros A m i v H.
- exact (xelements_correct m i xH nil H).
+ generalize (xelements_correct m i xH nil H). rewrite prev_append_prev. exact id.
Qed.
- Fixpoint xget (A : Type) (i j : positive) (m : t A) {struct j} : option A :=
- match i, j with
- | _, xH => get i m
- | xO ii, xO jj => xget ii jj m
- | xI ii, xI jj => xget ii jj m
- | _, _ => None
- end.
-
- Lemma xget_diag :
- forall (A : Type) (i : positive) (m1 m2 : t A) (o : option A),
- xget i i (Node m1 o m2) = o.
- Proof.
- induction i; intros; simpl; auto.
- Qed.
-
- Lemma xget_left :
- forall (A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
- xget i (append j (xO xH)) m1 = Some v -> xget i j (Node m1 o m2) = Some v.
- Proof.
- induction j; intros; destruct i; simpl; simpl in H; auto; try congruence.
- destruct i; congruence.
- Qed.
-
- Lemma xget_right :
- forall (A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
- xget i (append j (xI xH)) m2 = Some v -> xget i j (Node m1 o m2) = Some v.
- Proof.
- induction j; intros; destruct i; simpl; simpl in H; auto; try congruence.
- destruct i; congruence.
- Qed.
+ Lemma in_xelements:
+ forall (A: Type) (m: t A) (i k: positive) (v: A) l,
+ In (k, v) (xelements m i l) ->
+ (exists j, k = prev (prev_append j i) /\ get j m = Some v) \/ In (k, v) l.
+ Proof.
+ induction m as [|l IHl o r IHr]; intros i j v k H.
+ right; exact H.
+ destruct o as [o|].
+ specialize (IHl _ _ _ _ H). destruct IHl as [(j' & -> & Hj')|[IHl|IHl]].
+ left. exists (xO j'). split. reflexivity. exact Hj'.
+ inv IHl. left. exists xH. split. reflexivity. reflexivity.
+ destruct (IHr _ _ _ _ IHl) as [(j' & -> & Hj') | IH]; clear IHr.
+ left. exists (xI j'). split. reflexivity. exact Hj'.
+ right; assumption.
+ specialize (IHl _ _ _ _ H). destruct IHl as [(j' & -> & Hj' )|IHl].
+ left. exists (xO j'). split. reflexivity. exact Hj'.
+ destruct (IHr _ _ _ _ IHl) as [(j' & -> & Hj') | IH]; clear IHr.
+ left. exists (xI j'). split. reflexivity. exact Hj'.
+ right; assumption.
+ Qed.
Lemma xelements_complete:
forall (A: Type) (m: t A) (i j : positive) (v: A) k,
- In (i, v) (xelements m j k) -> xget i j m = Some v \/ In (i, v) k.
- Proof.
- induction m; simpl; intros.
- auto.
- destruct o.
- edestruct IHm1; eauto. left; apply xget_left; auto.
- destruct H0. inv H0. left; apply xget_diag.
- edestruct IHm2; eauto. left; apply xget_right; auto.
- edestruct IHm1; eauto. left; apply xget_left; auto.
- edestruct IHm2; eauto. left; apply xget_right; auto.
- Qed.
-
- Lemma get_xget_h :
- forall (A: Type) (m: t A) (i: positive), get i m = xget i xH m.
+ In (prev_append j i, v) (xelements m j k) -> get i m = Some v \/ In (prev_append j i, v) k.
Proof.
- destruct i; simpl; auto.
+ intros A m i j v k H.
+ apply in_xelements in H. destruct H as [(j' & EQ & Hj')|H].
+ rewrite prev_append_prev in EQ. apply prev_append_inj in EQ. left; congruence.
+ right; assumption.
Qed.
Theorem elements_complete:
forall (A: Type) (m: t A) (i: positive) (v: A),
In (i, v) (elements m) -> get i m = Some v.
Proof.
- intros A m i v H. unfold elements in H.
- edestruct xelements_complete; eauto.
- rewrite get_xget_h. auto.
- contradiction.
- Qed.
-
- Lemma in_xelements:
- forall (A: Type) (m: t A) (i k: positive) (v: A) l,
- In (k, v) (xelements m i l) ->
- (exists j, k = append i j) \/ In (k, v) l.
- Proof.
- induction m; simpl; intros.
- auto.
- destruct o.
- edestruct IHm1 as [[j EQ] | IN]; eauto.
- rewrite <- append_assoc_0 in EQ. left; econstructor; eauto.
- destruct IN.
- inv H0. left; exists xH; symmetry; apply append_neutral_r.
- edestruct IHm2 as [[j EQ] | IN]; eauto.
- rewrite <- append_assoc_1 in EQ. left; econstructor; eauto.
- edestruct IHm1 as [[j EQ] | IN]; eauto.
- rewrite <- append_assoc_0 in EQ. left; econstructor; eauto.
- edestruct IHm2 as [[j EQ] | IN']; eauto.
- rewrite <- append_assoc_1 in EQ. left; econstructor; eauto.
+ unfold elements. intros A m i v H.
+ change i with (prev_append 1 i) in H.
+ destruct (xelements_complete _ _ _ _ _ H) as [K|()]. exact K.
Qed.
Definition xkeys (A: Type) (m: t A) (i: positive) (l: list (positive * A)) :=
@@ -769,53 +717,50 @@ Module PTree <: TREE.
Lemma in_xkeys:
forall (A: Type) (m: t A) (i k: positive) l,
In k (xkeys m i l) ->
- (exists j, k = append i j) \/ In k (List.map fst l).
+ (exists j, k = prev (prev_append j i)) \/ In k (List.map fst l).
Proof.
unfold xkeys; intros.
- exploit list_in_map_inv; eauto. intros [[k1 v1] [EQ IN]].
- simpl in EQ; subst k1.
- exploit in_xelements; eauto. intros [EX | IN'].
- auto.
- right. change k with (fst (k, v1)). apply List.in_map; auto.
- Qed.
-
- Lemma append_injective:
- forall i j1 j2, append i j1 = append i j2 -> j1 = j2.
- Proof.
- induction i; simpl; intros.
- apply IHi. congruence.
- apply IHi. congruence.
- auto.
+ apply (list_in_map_inv) in H. destruct H as ((j, v) & -> & H).
+ change j with (prev_append 1 j) in H. apply in_xelements in H.
+ destruct H as [(j' & Hj' & _) | H]. simpl in Hj'; subst j.
+ left. simpl. exists j'. reflexivity.
+ right. apply in_map. exact H.
Qed.
Lemma xelements_keys_norepet:
forall (A: Type) (m: t A) (i: positive) l,
- (forall k v, get k m = Some v -> ~In (append i k) (List.map fst l)) ->
+ (forall k v, get k m = Some v -> ~In (prev (prev_append k i)) (List.map fst l)) ->
list_norepet (List.map fst l) ->
list_norepet (xkeys m i l).
Proof.
- unfold xkeys; induction m; simpl; intros.
+ unfold xkeys.
+ intros A m.
+ induction m as [|l Hl o r Hr]; intros i elem H NR.
auto.
- destruct o.
- apply IHm1.
- intros; red; intros IN. rewrite <- append_assoc_0 in IN. simpl in IN; destruct IN.
- exploit (append_injective i k~0 xH). rewrite append_neutral_r. auto.
- congruence.
- exploit in_xkeys; eauto. intros [[j EQ] | IN].
- rewrite <- append_assoc_1 in EQ. exploit append_injective; eauto. congruence.
- elim (H (xO k) v); auto.
- simpl. constructor.
- red; intros IN. exploit in_xkeys; eauto. intros [[j EQ] | IN'].
- rewrite <- append_assoc_1 in EQ.
- exploit (append_injective i j~1 xH). rewrite append_neutral_r. auto. congruence.
- elim (H xH a). auto. rewrite append_neutral_r. auto.
- apply IHm2; auto. intros. rewrite <- append_assoc_1. eapply H; eauto.
- apply IHm1.
- intros; red; intros IN. rewrite <- append_assoc_0 in IN.
- exploit in_xkeys; eauto. intros [[j EQ] | IN'].
- rewrite <- append_assoc_1 in EQ. exploit append_injective; eauto. congruence.
- elim (H (xO k) v); auto.
- apply IHm2; auto. intros. rewrite <- append_assoc_1. eapply H; eauto.
+ destruct o as [o|].
+ - apply Hl.
+ intros k v Hkv IN.
+ destruct IN as [IN | IN].
+ rewrite prev_append_prev in IN. simpl in IN. apply prev_append_inj in IN. discriminate.
+ apply in_xkeys in IN. destruct IN as [(j & EQ) | IN].
+ rewrite !prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate.
+ elim (H (xO k) v); auto; fail.
+ simpl. constructor.
+ intros IN.
+ apply in_xkeys in IN. destruct IN as [(j & EQ) | IN].
+ rewrite !prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate.
+ elim (H xH o); auto; fail.
+ apply Hr; auto.
+ intros k.
+ exact (H (xI k)).
+ - apply Hl.
+ intros k v Hkv IN.
+ apply in_xkeys in IN. destruct IN as [(j & EQ) | IN].
+ rewrite !prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate.
+ exact (H (xO k) _ Hkv IN).
+ apply Hr; auto.
+ intros k.
+ exact (H (xI k)).
Qed.
Theorem elements_keys_norepet:
@@ -908,12 +853,12 @@ Module PTree <: TREE.
match m with
| Leaf => v
| Node l None r =>
- let v1 := xfold f (append i (xO xH)) l v in
- xfold f (append i (xI xH)) r v1
+ let v1 := xfold f (xO i) l v in
+ xfold f (xI i) r v1
| Node l (Some x) r =>
- let v1 := xfold f (append i (xO xH)) l v in
- let v2 := f v1 i x in
- xfold f (append i (xI xH)) r v2
+ let v1 := xfold f (xO i) l v in
+ let v2 := f v1 (prev i) x in
+ xfold f (xI i) r v2
end.
Definition fold (A B : Type) (f: B -> positive -> A -> B) (m: t A) (v: B) :=