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

1 files changed, 26 insertions, 0 deletions

diff --git a/lib/Maps.v b/lib/Maps.v
index 255ce448..bd5c0e9f 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -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.