diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-10-27 09:23:19 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-10-27 09:23:19 +0000 |
commit | b54721f58c2ecb65ce554d8b34f214d5121a2b0c (patch) | |
tree | 01bc71f3e5e6b1681dac76de97ab925e005cc2c4 /lib/Maps.v | |
parent | 63cc20f9ddb18bebae523c46438abdf2a4b140d4 (diff) | |
download | compcert-b54721f58c2ecb65ce554d8b34f214d5121a2b0c.tar.gz compcert-b54721f58c2ecb65ce554d8b34f214d5121a2b0c.zip |
Various algorithmic improvements that reduce compile times (thanks Alexandre Pilkiewicz):
- Lattice: preserve sharing in "combine" operation
- Kildall: use splay heaps (lib/Heaps.v) for node sets
- RTLgen: add a "nop" before loops so that natural enumeration of nodes
coincides with (reverse) postorder
- Maps: add PTree.map1 operation, use it in RTL and LTL.
- Driver: increase minor heap size
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1543 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Maps.v')
-rw-r--r-- | lib/Maps.v | 24 |
1 files changed, 22 insertions, 2 deletions
@@ -98,6 +98,13 @@ Module Type TREE. forall (A B: Type) (f: elt -> A -> B) (i: elt) (m: t A), get i (map f m) = option_map (f i) (get i m). + (** Same as [map], but the function does not receive the [elt] argument. *) + Variable map1: + forall (A B: Type), (A -> B) -> t A -> t B. + Hypothesis gmap1: + forall (A B: Type) (f: A -> B) (i: elt) (m: t A), + get i (map1 f m) = option_map f (get i m). + (** Applying a function pairwise to all data of two trees. *) Variable combine: forall (A: Type), (option A -> option A -> option A) -> t A -> t A -> t A. @@ -492,6 +499,19 @@ Module PTree <: TREE. rewrite append_neutral_l; auto. Qed. + Fixpoint map1 (A B: Type) (f: A -> B) (m: t A) {struct m} : t B := + match m with + | Leaf => Leaf + | Node l o r => Node (map1 f l) (option_map f o) (map1 f r) + end. + + Theorem gmap1: + forall (A B: Type) (f: A -> B) (i: elt) (m: t A), + get i (map1 f m) = option_map f (get i m). + Proof. + induction i; intros; destruct m; simpl; auto. + Qed. + Definition Node' (A: Type) (l: t A) (x: option A) (r: t A): t A := match l, x, r with | Leaf, None, Leaf => Leaf @@ -1091,13 +1111,13 @@ Module PMap <: MAP. Qed. Definition map (A B : Type) (f : A -> B) (m : t A) : t B := - (f (fst m), PTree.map (fun _ => f) (snd m)). + (f (fst m), PTree.map1 f (snd m)). Theorem gmap: forall (A B: Type) (f: A -> B) (i: positive) (m: t A), get i (map f m) = f(get i m). Proof. - intros. unfold map. unfold get. simpl. rewrite PTree.gmap. + intros. unfold map. unfold get. simpl. rewrite PTree.gmap1. unfold option_map. destruct (PTree.get i (snd m)); auto. Qed. |