Module MapsC

Require Import LinkingC.
Require Import CoqlibC Maps Errors ASTC.
Require Import sflib.
Require Import RelationClasses.

Require Export Maps.

Set Implicit Arguments.

Local Open Scope o_monad_scope.

Fixpoint xfilter_map (A B : Type) (f : positive -> A -> option B) (m : PTree.t A) (i : positive)
         {struct m} : PTree.t B :=
  match m with
  | PTree.Leaf => PTree.Leaf
  | PTree.Node l o r => PTree.Node (xfilter_map f l (xO i))
                                  (match o with None => None | Some x => (f (PTree.prev i) x) end)
                                  (xfilter_map f r (xI i))
  end.

Lemma xfilter_map_get:
  forall (A B: Type) (f: positive -> A -> option B) (i j : positive) (m: PTree.t A),
    PTree.get i (xfilter_map f m j) = o_bind (PTree.get i m) (f (PTree.prev (PTree.prev_append i j))).
Proof.
induction i; intros; destruct m; simpl; auto. des_ifs. Qed.

Definition PTree_filter_map A B (f: positive -> A -> option B) (m: PTree.t A): PTree.t B := xfilter_map f m 1.

About PTree.gmap.

Lemma PTree_filter_map_spec
      A B (f: positive -> A -> option B) i m:
      (PTree_filter_map f m) ! i = o_bind (m ! i) (f i).
Proof.
  unfold PTree_filter_map. rewrite xfilter_map_get. f_equal. rewrite PTree.prev_append_prev. ss.
Qed.

About PTree.filter1.
Definition PTree_filter_key A (f: positive -> bool) (m: PTree.t A): PTree.t A :=
  PTree_filter_map (fun k v => if f k then Some v else None) m.

Lemma PTree_filter_key_spec
      A (f: positive -> bool) i (m: PTree.t A):
      (PTree_filter_key f m) ! i = assertion (f i); m ! i.
Proof.
  unfold PTree_filter_key. rewrite PTree_filter_map_spec. uo. des_ifs.
Qed.

Lemma PTree_elements_map
      X Y (f: X -> Y) xm:
    map (update_snd f) (PTree.elements xm) = PTree.elements (PTree.map (fun _ => f) xm).
Proof.
  unfold PTree.elements. unfold PTree.map. generalize 1%positive.
  assert(LIST: [] = map (update_snd f) ([]: list (prod positive X))) by ss.
  revert LIST. generalize ([]: list (prod positive X)) as lx. generalize ([]: list (prod positive Y)) as ly.
  induction xm; ii; ss. cbn in *. destruct o; ss; erewrite IHxm1; ss; erewrite IHxm2; ss.
Qed.