diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-26 08:13:20 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-26 08:13:20 +0000 |
commit | 440a0bf9ab0cae2372e339cca081b01e5551e332 (patch) | |
tree | 1a5a02e48696b98f716407f87a12064509760c8e /lib | |
parent | 132e36fa0be63eb5672eda9168403d3fb74af2fa (diff) | |
download | compcert-440a0bf9ab0cae2372e339cca081b01e5551e332.tar.gz compcert-440a0bf9ab0cae2372e339cca081b01e5551e332.zip |
Memdata: cleanup continued
Maps: add filter1 operation (could be useful some day)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1903 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Maps.v | 26 |
1 files changed, 26 insertions, 0 deletions
@@ -108,6 +108,14 @@ Module Type TREE. forall (A B: Type) (f: A -> B) (i: elt) (m: t A), get i (map1 f m) = option_map f (get i m). + (** Filtering data that match a given predicate. *) + Variable filter1: + forall (A: Type), (A -> bool) -> t A -> t A. + Hypothesis gfilter1: + forall (A: Type) (pred: A -> bool) (i: elt) (m: t A), + get i (filter1 pred m) = + match get i m with None => None | Some x => if pred x then Some x else None end. + (** 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. @@ -537,6 +545,24 @@ Module PTree <: TREE. destruct i; simpl; auto; rewrite gleaf; auto. Qed. + Fixpoint filter1 (A: Type) (pred: A -> bool) (m: t A) {struct m} : t A := + match m with + | Leaf => Leaf + | Node l o r => + let o' := match o with None => None | Some x => if pred x then o else None end in + Node' (filter1 pred l) o' (filter1 pred r) + end. + + Theorem gfilter1: + forall (A: Type) (pred: A -> bool) (i: elt) (m: t A), + get i (filter1 pred m) = + match get i m with None => None | Some x => if pred x then Some x else None end. + Proof. + intros until m. revert m i. induction m; simpl; intros. + rewrite gleaf; auto. + rewrite gnode'. destruct i; simpl; auto. destruct o; auto. + Qed. + Section COMBINE. Variable A: Type. |