diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-09-20 13:17:50 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-09-20 13:17:50 +0000 |
commit | 719d2c04a005714b3a1a1e838ffc653d65da662b (patch) | |
tree | 997d32925c5dbf0015c217897155a164b005813e /lib/Maps.v | |
parent | 76ea1108be6f8b4ba9dc0118a13f685bcb62bc2b (diff) | |
download | compcert-719d2c04a005714b3a1a1e838ffc653d65da662b.tar.gz compcert-719d2c04a005714b3a1a1e838ffc653d65da662b.zip |
Small improvements in compilation times for the register allocation pass.
Maps.v: add a PTree.fold1 operation that doesn't maintain the key.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2329 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Maps.v')
-rw-r--r-- | lib/Maps.v | 39 |
1 files changed, 39 insertions, 0 deletions
@@ -141,6 +141,13 @@ Module Type TREE. forall (A B: Type) (f: B -> elt -> A -> B) (v: B) (m: t A), fold f m v = List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v. + (** Same as [fold], but the function does not receive the [elt] argument. *) + Variable fold1: + forall (A B: Type), (B -> A -> B) -> t A -> B -> B. + Hypothesis fold1_spec: + forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A), + fold1 f m v = + List.fold_left (fun a p => f a (snd p)) (elements m) v. End TREE. (** * The abstract signatures of maps *) @@ -932,6 +939,38 @@ Module PTree <: TREE. intros. unfold fold, elements. rewrite <- xfold_xelements. auto. Qed. + Fixpoint fold1 (A B: Type) (f: B -> A -> B) (m: t A) (v: B) {struct m} : B := + match m with + | Leaf => v + | Node l None r => + let v1 := fold1 f l v in + fold1 f r v1 + | Node l (Some x) r => + let v1 := fold1 f l v in + let v2 := f v1 x in + fold1 f r v2 + end. + + Lemma fold1_xelements: + forall (A B: Type) (f: B -> A -> B) m i v l, + List.fold_left (fun a p => f a (snd p)) l (fold1 f m v) = + List.fold_left (fun a p => f a (snd p)) (xelements m i l) v. + Proof. + induction m; intros. + simpl. auto. + destruct o; simpl. + rewrite <- IHm1. simpl. rewrite <- IHm2. auto. + rewrite <- IHm1. rewrite <- IHm2. auto. + Qed. + + Theorem fold1_spec: + forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A), + fold1 f m v = + List.fold_left (fun a p => f a (snd p)) (elements m) v. + Proof. + intros. apply fold1_xelements with (l := @nil (positive * A)). + Qed. + End PTree. (** * An implementation of maps over type [positive] *) |